preprint · arXiv (Cornell University) · 2022

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

Quang Loc Le, Jun Sun, Pham, Long H., Shengchao Qin

Cited by 1Open access

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.

Cite this paper

APA 7

Le, Q. L., Sun, J., Pham, L. H., & Qin, S. (2022). S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs. arXiv (Cornell University). https://doi.org/10.48550/arxiv.2209.09327

MLA 9

Le, Quang Loc, et al. “S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs.” arXiv (Cornell University), 2022, https://doi.org/10.48550/arxiv.2209.09327.

Chicago

Le, Quang Loc, Jun Sun, Long H. Pham, and Shengchao Qin. 2022. “S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs.” arXiv (Cornell University). https://doi.org/10.48550/arxiv.2209.09327.

Harvard

Le, Q.L. et al. (2022) ‘S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs’, arXiv (Cornell University). Available at: https://doi.org/10.48550/arxiv.2209.09327.

BibTeX

@misc{le2022s2td,
  title = {{S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs}},
  author = {Le, Quang Loc and Sun, Jun and Pham, Long H. and Qin, Shengchao},
  journal = {arXiv (Cornell University)},
  year = {2022},
  doi = {10.48550/arxiv.2209.09327}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.