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

The entailment between separation logic formulae with inductive predicates (also known as symbolic heaps) has been shown to be decidable for a large class of inductive definitions. Recently, a 2EXPTIME algorithm has been proposed, however no precise lower bound is known (although a EXPTIME-hard bound for this problem has been established). In this paper, we show that deciding entailment between predicate atoms is 2EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines.

The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions (ADSLlowerbound.pdf)650KiB

Mon 20 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

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