APLAS 2024
Tue 22 - Fri 25 October 2024 Kyoto
Thu 24 Oct 2024 11:30 - 12:00 at Yamauchi Hall - Logic Chair(s): Daan Leijen

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 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

10:30 - 12:00
LogicResearch Papers at Yamauchi Hall
Chair(s): Daan Leijen Microsoft Research
10:30
30m
Talk
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
30m
Talk
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
30m
Talk
Relative Completeness of Incorrectness Separation Logic
Research Papers
Yeonseok Lee Nagoya University, Koji Nakazawa Graduate School of Informatics, Nagoya University
File Attached