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
- scientific article; zbMATH DE number 1706226 (Why is no real title available?)
- Correct code containing containers
- scientific article; zbMATH DE number 2088927 (Why is no real title available?)
- 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?)
- scientific article; zbMATH DE number 2011463 (Why is no real title available?)
- 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)
