S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs

TL;DR

S2TD is a novel verifier for heap-manipulating programs that uses an extended separation logic with cyclic proofs to efficiently detect bugs and avoid false positives, outperforming existing tools.

Contribution

It introduces a new verifier, S2TD, which encodes programs as CHC with extended separation logic and employs cyclic proofs for improved bug detection in heap programs.

Findings

S2TD outperforms state-of-the-art verifiers in effectiveness.

S2TD is more efficient than most existing tools.

S2TD precisely specifies de-allocated heaps to reduce false positives.

Abstract

Heap-manipulating programs are known to be challenging to reason about. We present a novel verifier for heap-manipulating programs called S2TD, which encodes programs systematically in the form of Constrained Horn Clauses (CHC) using a novel extension of separation logic (SL) with recursive predicates and dangling predicates. S2TD actively explores cyclic proofs to address the path explosion problem. S2TD differentiates itself from existing CHC-based verifiers by focusing on heap-manipulating programs and employing cyclic proof to efficiently verify or falsify them with counterexamples. Compared with existing SL-based verifiers, S2TD precisely specifies the heaps of de-allocated pointers to avoid false positives in reasoning about the presence of bugs. S2TD has been evaluated using a comprehensive set of benchmark programs from the SV-COMP repository. The results show that S2TD is more effective than state-of-art program verifiers and is more efficient than most of them.