Field constraint analysis

Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin Rinard

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings
Pages157-173
Number of pages17
Volume3855 LNCS
StatePublished - 2006
Event7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006 - Charleston, SC, United States
Duration: Jan 8 2006Jan 10 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3855 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006
CountryUnited States
CityCharleston, SC
Period1/8/061/10/06

Fingerprint

Data structures
Data Structures
Information Systems
Backbone
Invariant
Logic
Symbolic Analysis
Shape Analysis
Soundness
Verify
Arbitrary

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Wies, T., Kuncak, V., Lam, P., Podelski, A., & Rinard, M. (2006). Field constraint analysis. In Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings (Vol. 3855 LNCS, pp. 157-173). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3855 LNCS).

Field constraint analysis. / Wies, Thomas; Kuncak, Viktor; Lam, Patrick; Podelski, Andreas; Rinard, Martin.

Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings. Vol. 3855 LNCS 2006. p. 157-173 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3855 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Wies, T, Kuncak, V, Lam, P, Podelski, A & Rinard, M 2006, Field constraint analysis. in Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings. vol. 3855 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3855 LNCS, pp. 157-173, 7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006, Charleston, SC, United States, 1/8/06.
Wies T, Kuncak V, Lam P, Podelski A, Rinard M. Field constraint analysis. In Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings. Vol. 3855 LNCS. 2006. p. 157-173. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Wies, Thomas ; Kuncak, Viktor ; Lam, Patrick ; Podelski, Andreas ; Rinard, Martin. / Field constraint analysis. Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings. Vol. 3855 LNCS 2006. pp. 157-173 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{41be2272f4ba45589705229ee029d764,
title = "Field constraint analysis",
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 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.",
author = "Thomas Wies and Viktor Kuncak and Patrick Lam and Andreas Podelski and Martin Rinard",
year = "2006",
language = "English (US)",
isbn = "3540311394",
volume = "3855 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "157--173",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings",

}

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

SN - 3540311394

SN - 9783540311393

VL - 3855 LNCS

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

ER -