Simulating reachability using first-order logic with applications to verification of linked data structures

Tal Lev-Ami; Neil Immerman; Thomas Reps; Mooly Sagiv; Siddharth Srivastava; Greta Yorsh

doi:10.2168/LMCS-5(2:12)2009

Tal Lev-Ami ; Neil Immerman ; Thomas Reps ; Mooly Sagiv ; Siddharth Srivastava et al. - Simulating reachability using first-order logic with applications to verification of linked data structures

lmcs:680 - Logical Methods in Computer Science, May 28, 2009, Volume 5, Issue 2 - https://doi.org/10.2168/LMCS-5(2:12)2009

Simulating reachability using first-order logic with applications to verification of linked data structuresArticle

Authors: Tal Lev-Ami ; Neil Immerman ; Thomas Reps ; Mooly Sagiv ; Siddharth Srivastava ; Greta Yorsh

This paper shows how to harness existing theorem provers for first-order logic to automatically verify safety properties of imperative programs that perform dynamic storage allocation and destructive updating of pointer-valued structure fields. One of the main obstacles is specifying and proving the (absence) of reachability properties among dynamically allocated cells. The main technical contributions are methods for simulating reachability in a conservative way using first-order formulas--the formulas describe a superset of the set of program states that would be specified if one had a precise way to express reachability. These methods are employed for semi-automatic program verification (i.e., using programmer-supplied loop invariants) on programs such as mark-and-sweep garbage collection and destructive reversal of a singly linked list. (The mark-and-sweep example has been previously reported as being beyond the capabilities of ESC/Java.)

https://doi.org/10.2168/LMCS-5(2:12)2009

Source: arXiv.org:0904.4902

Volume: Volume 5, Issue 2

Published on: May 28, 2009

Imported on: April 2, 2006

Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.3.1,F.3.2,F.4.1

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Sources:

[1] zbMATH Open.

Bibliographic References

10 Documents citing this article

Arshavir Ter-Gabrielyan;Alexander J. Summers;Peter Müller, 2019, Modular verification of heap reachability properties in separation logic, Proceedings of the ACM on Programming Languages, 3, OOPSLA, pp. 1-28, 10.1145/3360547, https://doi.org/10.1145/3360547.

Xu Lu;Zhenhua Duan;Cong Tian;Hongwei Du, 2018, Verify heaps via unified model checking, Theoretical Computer Science, 819, pp. 35-49, 10.1016/j.tcs.2017.09.025, https://doi.org/10.1016/j.tcs.2017.09.025.

Christof Löding;P. Madhusudan;Lucas Peña, 2017, Foundations for natural proofs and quantifier instantiation, Proceedings of the ACM on Programming Languages, 2, POPL, pp. 1-30, 10.1145/3158098, https://doi.org/10.1145/3158098.

Thomas Schwentick;Thomas Zeume, 2016, Dynamic complexity, ACM SIGLOG News, 3, 2, pp. 30-52, 10.1145/2948896.2948899, https://doi.org/10.1145/2948896.2948899.

Christoph Gladisch;Shmuel Tyszberowicz, 2015, Specifying linked data structures in JML for combining formal verification and testing, Science of Computer Programming, 107-108, pp. 19-40, 10.1016/j.scico.2015.02.005.

Aboubakr Achraf El Ghazi;Mattias Ulbrich;Christoph Gladisch;Shmuel Tyszberowicz;Mana Taghdiri, Lecture notes in computer science, JKelloy: A Proof Assistant for Relational Specifications of Java Programs, pp. 173-187, 2014, 10.1007/978-3-319-06200-6_13.

Matthias Horbach;Viorica Sofronie-Stokkermans, Lecture notes in computer science, Locality Transfer: From Constrained Axiomatizations to Reachability Predicates, pp. 192-207, 2014, 10.1007/978-3-319-08587-6_14.

Christoph Gladisch;Shmuel Tyszberowicz, Lecture notes in computer science, Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking, pp. 99-114, 2013, 10.1007/978-3-642-41071-0_8.

Shachar Itzhaky;Anindya Banerjee;Neil Immerman;Aleksandar Nanevski;Mooly Sagiv, Lecture notes in computer science, Effectively-Propositional Reasoning about Reachability in Linked Data Structures, pp. 756-772, 2013, 10.1007/978-3-642-39799-8_53, https://doi.org/10.1007/978-3-642-39799-8_53.

Mattias Ulbrich;Ulrich Geilmann;Aboubakr Achraf El Ghazi;Mana Taghdiri, Lecture notes in computer science, A Proof Assistant for Alloy Specifications, pp. 422-436, 2012, 10.1007/978-3-642-28756-5_29, https://doi.org/10.1007/978-3-642-28756-5_29.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1496 times.

This article's PDF has been downloaded 295 times.