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

Quang Loc Le, Jun Sun, Long H. Pham +1

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 systematicall…