Relative Completeness of Incorrectness Separation Logic
Incorrectness Separation Logic (ISL) is a proof system that is tailored specifically to resolve problems of under-approximation in programs that manipulate heaps, and it primarily focuses on bug detection. This approach is different from the over-approximation methods that are used in traditional logics such as Hoare Logic or Separation Logic. Although the soundness of ISL has been established, its completeness remains unproven. In this study, we establish relative completeness by leveraging the expressiveness of the weakest postconditions; expressiveness is a factor that is critical to demonstrating relative completeness in Reverse Hoare Logic. In our ISL framework, we allow for infinite disjunctions in disjunctive normal forms, where each clause comprises finite symbolic heaps with existential quantifiers. To compute the weakest postconditions in ISL, we introduce a canonicalization that includes variable aliasing.
slides_241024 (aplas2024_slides_LEE.pdf) | 462KiB |
Thu 24 OctDisplayed time zone: Osaka, Sapporo, Tokyo change
10:30 - 12:00 | |||
10:30 30mTalk | Effective Search Space Pruning for Testing Deep Neural Networks Research Papers Bala Rangaya Singapore University of Technology and Design, Eugene Sng Ministry of Defence of Singapore, Minh-Thai Trinh Illinois Advanced Research Center at Singapore Ltd. | ||
11:00 30mTalk | Non-deterministic, probabilistic, and quantum effects through the lens of event structures Research Papers Vitor Fernandes University of Minho, Marc de Visme Université Paris-Saclay, CNRS, INRIA-SIF, LMF, Benoît Valiron Université Paris-Saclay, CNRS, CentraleSupélec, LMF | ||
11:30 30mTalk | Relative Completeness of Incorrectness Separation Logic Research Papers File Attached |