Verification conditions are code

DOI10.1007/s00236-006-0029-5zbMath1106.68066OpenAlexW2117210984MaRDI QIDQ855274

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)

Uses Software

• JML
• Spec#
• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theoretical basis for stepwise refinement and the programming calculus
• Predicative methodology
• An axiomatic definition of the programming language Pascal
• Predicative programming Part I
• Laws of programming
• Unification: a multidisciplinary survey
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• The Multiple Assignment Statement
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Refinement Calculus
• An axiomatic basis for computer programming

This page was built for publication: Verification conditions are code