Field constraint analysis
Wies T, Kuncak V, Lam P, Podelski A, Rinard M. 2006. Field constraint analysis. 7th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 3855, 157–173.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Scopus indexed
Author
Wies, ThomasISTA;
Kuncak, Viktor;
Lam, Patrick;
Podelski, Andreas;
Rinard, Martin
Series Title
LNCS
Abstract
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 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. 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.
Publishing Year
Date Published
2006-01-01
Proceedings Title
7th International Conference on Verification, Model Checking, and Abstract Interpretation
Publisher
Springer
Volume
3855
Page
157 - 173
Conference
VMCAI: Verification, Model Checking and Abstract Interpretation
Conference Location
Charleston, SC, United States
Conference Date
2006-01-08 – 2006-01-10
IST-REx-ID
Cite this
Wies T, Kuncak V, Lam P, Podelski A, Rinard M. Field constraint analysis. In: 7th International Conference on Verification, Model Checking, and Abstract Interpretation. Vol 3855. Springer; 2006:157-173. doi:10.1007/11609773_11
Wies, T., Kuncak, V., Lam, P., Podelski, A., & Rinard, M. (2006). Field constraint analysis. In 7th International Conference on Verification, Model Checking, and Abstract Interpretation (Vol. 3855, pp. 157–173). Charleston, SC, United States: Springer. https://doi.org/10.1007/11609773_11
Wies, Thomas, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard. “Field Constraint Analysis.” In 7th International Conference on Verification, Model Checking, and Abstract Interpretation, 3855:157–73. Springer, 2006. https://doi.org/10.1007/11609773_11.
T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard, “Field constraint analysis,” in 7th International Conference on Verification, Model Checking, and Abstract Interpretation, Charleston, SC, United States, 2006, vol. 3855, pp. 157–173.
Wies T, Kuncak V, Lam P, Podelski A, Rinard M. 2006. Field constraint analysis. 7th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 3855, 157–173.
Wies, Thomas, et al. “Field Constraint Analysis.” 7th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 3855, Springer, 2006, pp. 157–73, doi:10.1007/11609773_11.