Building high integrity applications with SPARK
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 1031980
- Software Verification and Analysis
- A bounded model checker for SPARK programs
- An integrated approach to high integrity software verification
- Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays
Cited in
(13)- Instrumenting a weakest precondition calculus for counterexample generation
- Verifying Whiley programs with Boogie
- Deductive verification of floating-point Java programs in KeY
- Using the SPARK toolset for showing the absence of run-time errors in safety-critical software
- Correct code containing containers
- Closing the loop: The influence of code analysis on design
- A bounded model checker for SPARK programs
- Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays
- scientific article; zbMATH DE number 1031980 (Why is no real title available?)
- High integrity Ravenscar
- Uniqueness types for efficient and verifiable aliasing-free embedded systems programming
- Formally verified roundoff error bounds on LogSumExp-based computations
- An integrated approach to high integrity software verification
This page was built for publication: Building high integrity applications with SPARK
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2947225)
