Reverse Hoare Logic

DOI10.1007/978-3-642-24690-6_12zbMath1349.03028OpenAlexW1599380282MaRDI QIDQ3095238

Edsko Devries, Vasileios Koutavas

Publication date: 28 October 2011

Published in: Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24690-6_12

Mathematics Subject Classification ID

Logic in computer science (03B70) Randomized algorithms (68W20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Loop verification with invariants and contracts ⋮ Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs ⋮ Adversarial logic ⋮ Reasoning about promises in weak memory models with event structures ⋮ RHLE: modular deductive verification of relational \(\forall \exists\) properties ⋮ On algebra of program correctness and incorrectness ⋮ Monadic second-order incorrectness logic for GP 2 ⋮ Incorrectness logic for graph programs

Uses Software

• Eiffel

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• An observationally complete program logic for imperative higher-order functions
• Program inversion in the refinement calculus
• Program inversion: More than fun!
• Ten years of Hoare's logic: A survey. II: Nondeterminism
• A probabilistic PDL
• Downward refinement and the efficiency of hierarchical problem solving
• Hoare logic and auxiliary variables
• Reasoning about probabilistic sequential programs
• An axiomatic definition of the programming language Pascal
• Ten Years of Hoare's Logic: A Survey—Part I
• Polymorphism and separation in hoare type theory
• An axiomatic basis for computer programming
• Integrated Formal Methods

This page was built for publication: Reverse Hoare Logic