Completeness of Cyclic Proofs for Symbolic Heaps

TL;DR

This paper introduces a cyclic proof system for symbolic heaps in separation logic, establishing its soundness, completeness, and a decision procedure for entailments with inductive definitions, advancing software verification methods.

Contribution

It presents a novel cyclic proof system for symbolic heaps with inductive definitions, proving its soundness, completeness, and providing a decision procedure for entailments.

Findings

The cyclic proof system is sound and complete for symbolic heaps.

Decidability of entailments with inductive definitions is established.

The decision procedure operates in nondeterministic double-exponential time.

Abstract

Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic proof system for symbolic heaps with general form of inductive definitions, and shows its soundness and completeness. The decision procedure for entailments of symbolic heaps with inductive definitions is also given. Decidability for entailments of symbolic heaps with inductive definitions is an important question. Completeness of cyclic proof systems is also an important question. The results of this paper answer both questions. The decision procedure is feasible since it is nondeterministic double-exponential time complexity.