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
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)0302-9743
ISSN (Electronic)1611-3349

Other

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Field constraint analysis'. Together they form a unique fingerprint.

Cite this