Verification Via Structure Simulation
N. Immerman, A. Rabinovich, T. Reps, M. Sagiv, and G. Yorsh
This paper shows how to harness decision procedures to automatically
verify safety properties of imperative programs that perform dynamic
storage allocation and destructive updating of structure fields.
Decidable logics that can express reachability properties
are used to state properties of linked data structures, while
guaranteeing that the verification method always terminates.
The main technical contribution is a method of structure simulation in
which a set of original structures that we wish to model, e.g.,
doubly linked lists, nested linked lists, binary trees, etc.,
are mapped to a set of tractable structures that can be
reasoned about using decidable logics.
Decidable logics that can express reachability are rather
limited in the data structures that they can directly model.
For instance, our examples use the logic MSO-E, which can
only model function graphs;
however, the simulation technique provides an indirect way
to model additional data structures.
(Click here to access the paper:
PostScript,
PDF.)