Fu Song

Tractability of Separation Logic with Inductive Definitions: Beyond Lists

2017 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

In 2011, Cook et al. showed that the satisfiability and entailment can be checked in polynomial time for a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. In …