Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse




Conference Paper

Field Constraint Analysis


Wies,  Thomas
Programming Logics, MPI for Informatics, Max Planck Society;

Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Wies, T., Kuncak, V., Lam, P., Podelski, A., & Rinard, M. C. (2006). Field Constraint Analysis. In Verification, Model Checking, and Abstract Interpretation: 7th International Conference, VMCAI 2006 (pp. 157-173). Berlin, Germany: Springer.

Cite as:
We introduce \emph{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 limits the range of analyzable data structures. Field constraint analysis permits \emph{non-deterministic} field constraints on cross-cutting fields, which allows the verificiation of invariants for 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.