Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic

被引：41

作者：

Raad, Azalea ^{[1
,2
]}

Berdine, Josh ^{[3
]}

Dang, Hoang-Hai ^{[1
,2
]}

Dreyer, Derek ^{[1
,2
]}

O'Hearn, Peter ^{[3
,4
]}

Villard, Jules ^{[3
]}

机构：

[1] Max Planck Inst Software Syst MPI SWS, Kaiserslautern, Germany

[2] Max Planck Inst Software Syst MPI SWS, Saarbrucken, Germany

[3] Facebook, London, England

[4] UCL, London, England

来源：

COMPUTER AIDED VERIFICATION, PT II | 2020年 / 12225卷

基金：

欧洲研究理事会;

关键词：

Program logics; Separation logic; Bug catching; SHAPE-ANALYSIS; STATIC ANALYSIS;

D O I：

10.1007/978-3-030-53291-8_14

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：225 / 252

页数：28

共 50 条

[11] Reasoning about Cloud Storage Systems Based on Separation Logic
Jin Z.
Wang H.-P.
Zhang B.-W.
Zhang L.
Cao Y.-Z.
Jisuanji Xuebao/Chinese Journal of Computers, 2020, 43 (12): : 2227 - 2240
[12] Reasoning about B+ Trees with Operational Semantics and Separation Logic
Sexton, Alan
Thielecke, Hayo
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 218 (355-369) : 355 - 369
[13] Diagrammatic Reasoning in Separation Logic
Ridsdale, M.
Jamnik, N.
Benton, N.
Berdine, J.
DIAGRAMMATIC REPRESENTATION AND INFERENCE, PROCEEDINGS, 2008, 5223 : 408 - +
[14] A LOGIC FOR REASONING ABOUT PROBABILITIES
FAGIN, R
HALPERN, JY
MEGIDDO, N
INFORMATION AND COMPUTATION, 1990, 87 (1-2) : 78 - 128
[15] A LOGIC FOR REASONING ABOUT SECURITY
GLASGOW, J
MACEWEN, G
PANANGADEN, P
ACM TRANSACTIONS ON COMPUTER SYSTEMS, 1992, 10 (03): : 226 - 264
[16] A logic for reasoning about ambiguity
Halpern, Joseph Y.
Kets, Willemien
ARTIFICIAL INTELLIGENCE, 2014, 209 : 1 - 10
[17] A logic for reasoning about responsibility
de Lima, Tiago
Royakkers, Lamber
Dignum, Frank
LOGIC JOURNAL OF THE IGPL, 2010, 18 (01) : 99 - 117
[18] A logic for reasoning about evidence
Halpern, Joseph Y.
Pucella, Riccardo
JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 2006, 26 : 1 - 34
[19] REASONING ABOUT UPDATE LOGIC
VANEIJCK, J
DEVRIES, FJ
JOURNAL OF PHILOSOPHICAL LOGIC, 1995, 24 (01) : 19 - 45
[20] A logic for reasoning about evidence
Halpern, Joseph Y.
Pucella, Riccardo
Journal of Artificial Intelligence Research, 2006, 26 : 1 - 34

← 1 2 3 4 5 →