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

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

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

• 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
• 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?)
• 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. II: Nondeterminism
• Ten Years of Hoare's Logic: A Survey—Part I

Cited in

(15)

• Reverse formalism 16
• Monadic second-order incorrectness logic for GP 2
• Incorrectness logic for graph programs
• Loop verification with invariants and contracts
• On algebra of program correctness and incorrectness
• 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
• Low-level reachability analysis based on formal logic
• Domain reasoning in TopKAT
• The autonomous data language -- concepts, design and formal verification
• A correctness and incorrectness program logic
• On the design of program logics
• Cyclic proofs in Hoare logic and its reverse

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)