Reverse Hoare logic

DOI10.1007/978-3-642-24690-6_12MaRDI QIDQ3095238zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Reasoning About States of Probabilistic Sequential Programs
• scientific article; zbMATH DE number 1500556
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• Hoare-style logic for unstructured programs
• scientific article; zbMATH DE number 2110621

Cites work

• scientific article; zbMATH DE number 4033710 (Why is no real title available?)
• scientific article; zbMATH DE number 1105469 (Why is no real title available?)
• scientific article; zbMATH DE number 1500556 (Why is no real title available?)
• A probabilistic PDL
• An axiomatic basis for computer programming
• An axiomatic definition of the programming language Pascal
• An observationally complete program logic for imperative higher-order functions
• Downward refinement and the efficiency of hierarchical problem solving
• Hoare logic and auxiliary variables
• Integrated Formal Methods
• Polymorphism and separation in Hoare type theory
• Program inversion in the refinement calculus
• Program inversion: More than fun!
• Reasoning about probabilistic sequential programs
• Ten Years of Hoare's Logic: A Survey—Part I
• Ten years of Hoare's logic: A survey. II: Nondeterminism

Cited in

(10)

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

Describes a project that uses

Uses Software

• Eiffel

This page was built for publication: Reverse Hoare logic

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