Lev-Ami, T.; Immerman, N.; Reps, T.; Sagiv, M.; Srivastava, S.; Yorsh, G. Simulating reachability using first-order logic with applications to verification of linked data structures. (English) Zbl 1135.68556 Nieuwenhuis, Robert (ed.), Automated deduction – CADE-20. 20th international conference on automated deduction, Tallinn, Estonia, July 22–27, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28005-7/pbk). Lecture Notes in Computer Science 3632. Lecture Notes in Artificial Intelligence, 99-115 (2005). Summary: 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 can actually arise. 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.)For the entire collection see [Zbl 1088.68008]. Cited in 10 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68P05 Data structures 68Q60 Specification and verification (program logics, model checking, etc.) PDFBibTeX XMLCite \textit{T. Lev-Ami} et al., Lect. Notes Comput. Sci. 3632, 99--115 (2005; Zbl 1135.68556) Full Text: DOI arXiv