On Field Constraint Analysis
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 ori...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30582 |
| _version_ | 1826194409639641088 |
|---|---|
| author | Wies, Thomas Kuncak, Viktor Lam, Patrick Podelski, Andreas Rinard, Martin |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Wies, Thomas Kuncak, Viktor Lam, Patrick Podelski, Andreas Rinard, Martin |
| author_sort | Wies, Thomas |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T09:55:40Z |
| id | mit-1721.1/30582 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T09:55:40Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/305822019-04-11T06:23:37Z On Field Constraint Analysis Wies, Thomas Kuncak, Viktor Lam, Patrick Podelski, Andreas Rinard, Martin Computer Architecture 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. 2005-12-22T02:40:34Z 2005-12-22T02:40:34Z 2005-11-03 MIT-CSAIL-TR-2005-072 MIT-LCS-TR-1010 http://hdl.handle.net/1721.1/30582 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 23 p. 22680509 bytes 928319 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Wies, Thomas Kuncak, Viktor Lam, Patrick Podelski, Andreas Rinard, Martin On Field Constraint Analysis |
| title | On Field Constraint Analysis |
| title_full | On Field Constraint Analysis |
| title_fullStr | On Field Constraint Analysis |
| title_full_unstemmed | On Field Constraint Analysis |
| title_short | On Field Constraint Analysis |
| title_sort | on field constraint analysis |
| url | http://hdl.handle.net/1721.1/30582 |
| work_keys_str_mv | AT wiesthomas onfieldconstraintanalysis AT kuncakviktor onfieldconstraintanalysis AT lampatrick onfieldconstraintanalysis AT podelskiandreas onfieldconstraintanalysis AT rinardmartin onfieldconstraintanalysis |