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 条
  • [1] Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
    Zilberstein, Noam
    Saliling, Angelina
    Silva, Alexandra
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (OOPSLA):
  • [2] Concurrent incorrectness separation logic
    Raad, Azalea
    Berdine, Josh
    Dreyer, Derek
    O'Hearn, Peter W.
    Proceedings of the ACM on Programming Languages, 2022, 6 (POPL)
  • [3] Concurrent Incorrectness Separation Logic
    Raad, Azalea
    Berdine, Josh
    Dreyer, Derek
    O'Hearn, Peter W.
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6
  • [4] Reasoning about Monotonicity in Separation Logic
    Timany, Amin
    Birkedal, Lars
    CPP '21: PROCEEDINGS OF THE 10TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2021, : 91 - 104
  • [5] Finding Real Bugs in Big Programs with Incorrectness Logic
    Quang Loc Le
    Raad, Azalea
    Villard, Jules
    Berdine, Josh
    Dreyer, Derek
    O'Hearn, Peter W.
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6 (OOPSLA):
  • [6] Relative Completeness of Incorrectness Separation Logic
    Lee, Yeonseok
    Nakazawa, Koji
    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2024, 2025, 15194 : 264 - 282
  • [7] Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
    Zilberstein, Noam
    Dreyer, Derek
    Silva, Alexandra
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (OOPSLA):
  • [8] Multimodal Separation Logic for Reasoning About Operational Semantics
    Dockins, Robert
    Appel, Andrew W.
    Hobor, Aquinas
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 218 : 5 - 20
  • [9] Quantitative Separation Logic A Logic for Reasoning about Probabilistic Pointer Programs
    Batz, Kevin
    Kaminski, Benjamin Lucien
    Katoen, Joost-Pieter
    Matheja, Christoph
    Noll, Thomas
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL):
  • [10] Regional logic for local reasoning about global invariants
    Banerjee, Anindya
    Naumann, David A.
    Rosenberg, Stan
    ECOOP 2008 - OBJECT-ORIENTED PROGRAMMING, PROCEEDINGS, 2008, 5142 : 387 - +
12345