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.
Author supplied keywords
Cite
CITATION STYLE
Raad, A., Berdine, J., Dang, H. H., Dreyer, D., O’Hearn, P., & Villard, J. (2020). Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12225 LNCS, pp. 225–252). Springer. https://doi.org/10.1007/978-3-030-53291-8_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
