An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic

TL;DR

This paper introduces a polynomial-time cyclic entailment procedure for a broad class of inductive predicates in separation logic, enabling efficient verification of complex data structures without backtracking.

Contribution

It presents a novel decision procedure that is both efficient and expressive, supporting a wide range of data structures in separation logic.

Findings

The procedure operates in polynomial time.

It supports complex data structures like nested lists, skip lists, and binary trees.

Experimental results show high efficiency on challenging problems.

Abstract

An efficient entailment proof system is essential to compositional verification using separation logic. Unfortunately, existing decision procedures are either inexpressive or inefficient. For example, Smallfoot is an efficient procedure but only works with hardwired lists and trees. Other procedures that can support general inductive predicates run exponentially in time as their proof search requires back-tracking to deal with a disjunction in the consequent. This paper presents a decision procedure to derive cyclic entailment proofs for general inductive predicates in polynomial time. Our procedure is efficient and does not require back-tracking; it uses normalisation rules that help avoid the introduction of disjunction in the consequent. Moreover, our decidable fragment is sufficiently expressive: It is based on compositional predicates and can capture a wide range of data structures, including sorted and nested list segments, skip lists with fast forward pointers, and binary search trees. We have implemented the proposal in a prototype tool and evaluated it over challenging problems taken from a recent separation logic competition. The experimental results confirm the efficiency of the proposed system.