Building high integrity applications with SPARK

DOI10.1017/CBO9781139629294MaRDI QIDQ2947225zbMATH OpenFDO

Authors John W. McCormick, Peter C. Chapin

Publication date 22 September 2015

zbMATH Keywords

preconditiontheorem provingprogram verificationassertionsSPARKAdapostconditionprogramming with contracts

Mathematics Subject Classification ID

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)

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

(11)

• Verifying Whiley programs with Boogie
• Deductive verification of floating-point Java programs in KeY
• scientific article; zbMATH DE number 2011463 (Why is no real title available?)
• An integrated approach to high integrity software verification
• scientific article; zbMATH DE number 2088927 (Why is no real title available?)
• Instrumenting a weakest precondition calculus for counterexample generation
• scientific article; zbMATH DE number 1706226 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

• GNATprove
• Alt-Ergo
• SPARK

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)