Write a Blog >>
Mon 20 Jan 2020 10:30 - 11:00 at Conde - Research Papers

At TACAS 2019, we published a decision procedure for the entailment problem for symbolic-heap separation logic with inductive definitions of bounded treewidth based on a novel abstraction we called the profile abstraction. Since then, we have discovered an incompleteness issue with that decision procedure, as well as a generalization of the profile abstraction that fixes the issue. In this article, we give a high-level discussion of the approach of our TACAS paper, identify the reason for its incompleteness, and explain the necessary changes to obtain a complete decision procedure while retaining the same asymptotic complexity. A complementary article with a full formalization of the extended decision procedure is currently under preparation.

Extending the Profile Abstraction for Complete Entailment Checking of Symbolic Heaps of Bounded Treewidth (main.pdf)657KiB

Mon 20 Jan

adsl-2020-papers
10:30 - 12:30: ADSL 2020 - Research Papers at Conde
adsl-2020-papers10:30 - 11:00
Research paper
File Attached
adsl-2020-papers11:00 - 11:30
Research paper
Denis MerigouxINRIA, Aymeric FromherzCarnegie Mellon University
File Attached
adsl-2020-papers11:30 - 12:00
Research paper
File Attached
adsl-2020-papers12:00 - 12:30
Research paper
Mnacho Echenim, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Nicolas Peltier
Pre-print File Attached