Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
复制标题
DOI：
10.1007/978-3-030-53291-8_14
复制
发表时间：
2020-06-16
期刊：
影响因子：
--
通讯作者：
Villard J
中科院分区：
文献类型：
--
作者：
Raad A;Berdine J;Dang HH;Dreyer D;O’Hearn P;Villard J
已经有大量的工作在本地推理证明没有错误，但没有证明他们的存在。我们提出了一个新的形式化框架，局部推理存在的错误，建立在两个互补的基础上：1）分离逻辑和2）不正确的逻辑。我们探索这个新的不正确分离逻辑（ISL）的理论，并使用它来推导出一个任意位置，过程内的符号执行分析，没有误报的建设。在这样做的过程中，我们朝着将模块化、可扩展的技术从程序验证转移到错误捕获的方向迈出了一步。
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.
登录
查看更多内容
影响因子：
1.8
作者：
Gorogiannis, Nikos;O'Hearn, Peter W.;Sergey, Ilya
通讯作者：
Sergey, Ilya
影响因子：
--
作者：
Ishtiaq, S;O'Hearn, PW
通讯作者：
O'Hearn, PW
DOI：
10.1007/978-3-540-24730-2_15
发表时间：
2004-01-01
期刊：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS
影响因子：
--
作者：
Clarke, E;Kroening, D;Lerda, F
通讯作者：
Lerda, F
影响因子：
22.7
作者：
Bessey, Al;Block, Ken;Engler, Dawson
通讯作者：
Engler, Dawson
影响因子：
--
作者：
Gardner, Philippa;Maffeis, Sergio;Smith, Gareth
通讯作者：
Smith, Gareth