O'Hearn, PW;
(2020)
Incorrectness logic.
Proceedings of the ACM on Programming Languages
, 4
, Article 10. 10.1145/3371078.
Preview |
Text
IL.pdf - Published Version Download (763kB) | Preview |
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.
Type: | Article |
---|---|
Title: | Incorrectness logic |
Open access status: | An open access version is available from UCL Discovery |
DOI: | 10.1145/3371078 |
Publisher version: | https://doi.org/10.1145/3371078 |
Language: | English |
Additional information: | © 2020 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/). |
Keywords: | Proofs, Bugs, Static Analysis |
UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
URI: | https://discovery.ucl.ac.uk/id/eprint/10095439 |
Archive Staff Only
View Item |