Reverse Hoare Logic
The work
| Authors | Edsko de Vries; Vasileios Koutavas |
|---|---|
| Type | inproceedings |
| Year | 2011 |
| Citekey | vries2011reverse |
Where it appeared
| Published in | Software Engineering and Formal Methods |
|---|---|
| Publisher | Springer Science+Business Media |
| Series | Lecture Notes in Computer Science |
| Pages | 155--171 |
Identifiers
| DOI | 10.1007/978-3-642-24690-6_12 |
|---|---|
| OpenAlex | W1599380282 |
| ISBN | 9783642246890 |
Access
| Landing page | https://doi.org/10.1007/978-3-642-24690-6_12 |
|---|
Abstract
We present a novel Hoare-style logic, called Reverse Hoare Logic, which can be used to reason about state reachability of imperative programs. This enables us to give natural specifications to randomized (deterministic or nondeterministic) algorithms. We give a proof system for the logic and use this to give simple formal proofs for a number of illustrative examples. We define a weakest postcondition calculus and use this to show that the proof system is sound and complete.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-24 00:00 UTC |
| Approved by | a person 2026-08-24 07:32 UTC |
Cite it as
@inproceedings{vries2011reverse,
title = {Reverse Hoare Logic},
author = {Edsko de Vries and Vasileios Koutavas},
year = {2011},
booktitle = {Software Engineering and Formal Methods},
pages = {155--171},
publisher = {Springer Science+Business Media},
series = {Lecture Notes in Computer Science},
isbn = {9783642246890},
doi = {10.1007/978-3-642-24690-6_12},
}
This record lives at https://refs.drheap.org/vries2011reverse/ and will keep doing so.