Reverse Hoare logic

DOI10.1007/978-3-642-24690-6_12zbMATH Open1349.03028OpenAlexW1599380282MaRDI QIDQ3095238FDOQ3095238

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (10)

• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
• 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
• 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

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)