TY - GEN
T1 - Field constraint analysis
AU - Wies, Thomas
AU - Kuncak, Viktor
AU - Lam, Patrick
AU - Podelski, Andreas
AU - Rinard, Martin
PY - 2006
Y1 - 2006
N2 - 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 limits the range of analyzable data structures. Field constraint analysis permits non-deterministic field constraints on crosscutting 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. 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.
AB - 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 limits the range of analyzable data structures. Field constraint analysis permits non-deterministic field constraints on crosscutting 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. 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.
UR - http://www.scopus.com/inward/record.url?scp=33745654319&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33745654319&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:33745654319
SN - 3540311394
SN - 9783540311393
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 157
EP - 173
BT - Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings
T2 - 7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006
Y2 - 8 January 2006 through 10 January 2006
ER -