2018/04/11 by Makoto Tatsuta, Tatsuta, Makoto, Koji Nakazawa +3
Computer Science · #03B70 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic in computer science #Logic, programming, and type systems #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1804.03938
openalex publication_date 2018/04/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.