@InProceedings{isl,
author="Raad, Azalea
and Berdine, Josh
and Dang, Hoang-Hai
and Dreyer, Derek
and O'Hearn, Peter
and Villard, Jules",
editor="Lahiri, Shuvendu K.
and Wang, Chao",
title="Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic",
booktitle="Computer Aided Verification",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="225--252",
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.",
isbn="978-3-030-53291-8"
}