@inproceedings{dd3c87796b3c40b9b3d4d4c04e670c5a,
title = "Simulating reachability using first-order logic with applications to verification of linked data structures",
abstract = "This paper shows how lo harness exisling Iheorcm provers for firslorder logic lo automatically verify safely properlies of imperative programs lhal 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.)",
author = "T. Lev-Ami and N. Immerman and T. Reps and M. Sagiv and S. Srivastava and G. Yorsh",
note = "Copyright: Copyright 2020 Elsevier B.V., All rights reserved.; 20th International Conference on Automated Deduction, CADE-20 ; Conference date: 22-07-2005 Through 27-07-2005",
year = "2005",
doi = "10.1007/11532231_8",
language = "English (US)",
isbn = "3540280057",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "99--115",
booktitle = "Automated Deduction - CADE-20 - 20th International Conference on Automated Deduction, Proceedings",
}