On Field Constraint Analysis

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

Citation

Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard. On field constraint analysis. Technical Report MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010, MIT CSAIL, November 2005. Full version of [52].

BibTex Entry

@techreport{WiesETAL05OnFieldConstraintAnalysis,
  author = {Thomas Wies and Viktor Kuncak and Patrick Lam and Andreas Podelski and Martin Rinard},
  title = {On Field Constraint Analysis},
  institution = {MIT CSAIL},
  year = 2005,
  month = {November},
  number = {MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010},
  note = {Full version of \cite{WiesETAL06FieldConstraintAnalysis}},
  abstract = {
  We introduce \emph{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.
}
}