O'Hearn, P;
Dreyer, D;
Villard, J;
Berdine, J;
Raad, A;
Dang, H;
(2020)
Local reasoning about the presence of bugs: Incorrectness Separation Logic.
In: Lahiri, S.K and Wang, C, (eds.)
CAV 2020: Computer Aided Verification.
(pp. pp. 225-252).
Springer: Los Angeles, CA, USA.
Preview |
Text
Raad2020_Chapter_LocalReasoningAboutThePresence.pdf - Published Version Download (982kB) | Preview |
Abstract
There has been a large body of work on local reasoning for proving the absence of bugs, but none for proving their presence. We present a new formal framework for local reasoning about the presence of bugs, building on two complementary foundations: 1) separation logic and 2) incorrectness logic. We explore the theory of this new incorrectness separation logic (ISL), and use it to derive a begin-anywhere, intra-procedural symbolic execution analysis that has no false positives by construction. In so doing, we take a step towards transferring modular, scalable techniques from the world of program verification to bug catching.
| Type: | Proceedings paper |
|---|---|
| Title: | Local reasoning about the presence of bugs: Incorrectness Separation Logic |
| Event: | International Conference on Computer Aided Verification |
| ISBN-13: | 978-3-030-53291-8 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-53291-8_14 |
| Publisher version: | https://doi.org/10.1007/978-3-030-53291-8_14 |
| Language: | English |
| Additional information: | This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. |
| Keywords: | Program logics · Separation logic · Bug catching |
| 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-pp.ucl.ac.uk/id/eprint/10115885 |
Archive Staff Only
 |
View Item |
