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: Saskatchewan, Central America change