Verification conditions are code

DOI10.1007/S00236-006-0029-5MaRDI QIDQ855274zbMATHOpenAlexFDO

Authors Andrew M. Gravell

Publication date 5 January 2007

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://eprints.soton.ac.uk/262472/1/vcs3preprint.pdf

zbMATH Keywords

Hoare logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification conditions for source-level imperative programs
• scientific article; zbMATH DE number 90777
• Logic programs as specifications in the inductive verification of logic programs
• Two theorems about the completeness of Hoare's logic
• scientific article; zbMATH DE number 3900131

Cites work

• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 53085 (Why is no real title available?)
• scientific article; zbMATH DE number 517333 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• A theoretical basis for stepwise refinement and the programming calculus
• An axiomatic basis for computer programming
• An axiomatic definition of the programming language Pascal
• Laws of programming
• Predicative methodology
• Predicative programming Part I
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Refinement Calculus
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I
• The Multiple Assignment Statement
• Unification: a multidisciplinary survey

Cited in

(6)

• Verification conditions for source-level imperative programs
• scientific article; zbMATH DE number 90777 (Why is no real title available?)
• scientific article; zbMATH DE number 1420791 (Why is no real title available?)
• Generation of correctness conditions for imperative programs
• A decomposition rule for the Hoare logic
• Explaining Verification Conditions

Describes a project that uses

Uses Software

• JML
• Spec#
• Nuprl

This page was built for publication: Verification conditions are code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q855274)