Building High Integrity Applications with SPARK

DOI10.1017/CBO9781139629294zbMath1328.68009MaRDI QIDQ2947225

Peter C. Chapin, John W. McCormick

Publication date: 22 September 2015

zbMATH Keywords

preconditiontheorem provingprogram verificationassertionsSPARKAdapostconditionprogramming with contracts

Mathematics Subject Classification ID

Theory of programming languages (68N15) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Instrumenting a weakest precondition calculus for counterexample generation ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Verifying Whiley programs with Boogie

Uses Software

• SPARK
• Alt-Ergo
• GNATprove

This page was built for publication: Building High Integrity Applications with SPARK