Building high integrity applications with SPARK
DOI10.1017/CBO9781139629294zbMATH Open1328.68009MaRDI QIDQ2947225FDOQ2947225
Authors: John W. McCormick, Peter C. Chapin 
Publication date: 22 September 2015
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
preconditiontheorem provingprogram verificationassertionsSPARKAdapostconditionprogramming with contracts
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cited In (11)
- Verifying Whiley programs with Boogie
- Deductive verification of floating-point Java programs in KeY
- Title not available (Why is that?)
- An integrated approach to high integrity software verification
- Title not available (Why is that?)
- Instrumenting a weakest precondition calculus for counterexample generation
- Title not available (Why is that?)
- Correct code containing containers
- A bounded model checker for SPARK programs
- Uniqueness types for efficient and verifiable aliasing-free embedded systems programming
- Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays
Uses Software
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)
