| |
VOLUME 5, ISSUE 2, PAPER 12
|
Simulating reachability using first-order logic with applications to verification of linked data structures
|
©Tal Lev-Ami, Tel-Aviv University
©Neil Immerman, University of Massachusetts, Amherst
©Thomas W Reps, University of Wisconsin, Madison
©Mooly Sagiv, Tel-Aviv University
©Siddharth Srivastava, University of Massachusetts, Amherst
©Greta Yorsh, Tel-Aviv University
|
Abstract
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.)
|
Publication date: May 28, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(2:12)2009
Hit Counts: 2348 |
 Creative Commons | |
