LCS Publication Details
Publication Title: On Field Constraint Analysis
Publication Author: Wies, Thomas
Additional Authors: Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin Rinard
LCS Document Number: MIT-LCS-TR-1010
Publication Date: 11-3-2005
LCS Group: Computer Architecture
Additional URL:
We introduce field constraint analysis, a new technique for verifying data structure invariants. A field constraint for a field is a formula specifying a set of objects to which the field can point. Field constraints enable the application of decidable logics to data structures which were originally beyond the scope of these logics, by verifying the backbone of the data structure and then verifying constraints on fields that cross-cut the backbone in arbitrary ways. Previously, such cross-cutting fields could only be verified when they were uniquely determined by the backbone, which significantly limited the range of analyzable data structures. Our field constraint analysis permits \\emph{non-deterministic} field constraints on cross-cutting fields, which allows to verify invariants of data structures such as skip lists. Non-deterministic field constraints also enable the verification of invariants between data structures, yielding an expressive generalization of static type declarations. The generality of our field constraints requires new techniques, which are orthogonal to the traditional use of structure simulation. We present one such technique and prove its soundness. We have implemented this technique as part of a symbolic shape analysis deployed in the context of the Hob system for verifying data structure consistency. Using this implementation we were able to verify data structures that were previously beyond the reach of similar techniques.
To obtain this publication:

To purchase a printed copy of this publication please contact MIT Document Services.