Incorrectness logic
The work
| Authors | Peter W. O'Hearn |
|---|---|
| Type | inproceedings |
| Year | 2020 |
| Also known as | ohearn2019incorrectness |
| Citekey | ohearn2020incorrectness |
Where it appeared
| Published in | Proceedings of the ACM on Programming Languages |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 4 |
| Issue | POPL |
| Pages | 10:1--10:32 |
Identifiers
| DOI | 10.1145/3371078 |
|---|---|
| OpenAlex | W3207402727 |
Access
| Free full text | https://dl.acm.org/doi/pdf/10.1145/3371078 |
|---|---|
| Landing page | https://doi.org/10.1145/3371078 |
Abstract
Program correctness and incorrectness are two sides of the same coin. As a programmer, even if you would like to have correctness, you might find yourself spending most of your time reasoning about incorrectness. This includes informal reasoning that people do while looking at or thinking about their code, as well as that supported by automated testing and static analysis tools. This paper describes a simple logic for program incorrectness which is, in a sense, the other side of the coin to Hoare's logic of correctness.
A copy is held
pdf, 745.2 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-21 05:49 UTC |
Cite it as
@inproceedings{ohearn2020incorrectness,
title = {Incorrectness logic},
author = {Peter W. O'Hearn},
year = {2020},
booktitle = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
pages = {10:1--10:32},
publisher = {Association for Computing Machinery},
doi = {10.1145/3371078},
}
This record lives at https://refs.drheap.org/ohearn2020incorrectness/ and will keep
doing so. It used to be called ohearn2019incorrectness, and those addresses still resolve to this one.