Name
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 limits the range of
analyzable data structures.
Field constraint analysis permits \emph{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.
|
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11609773_11 | Verification, Model Checking and Abstract Interpretation |
Keywords | Field | DocType |
verifying data structure invariants,cross-cutting field,field constraint,verifying constraint,analyzable data structure,verifying data structure consistency,non-deterministic field constraint,field constraint analysis,data structure,new technique,shape analysis,skip list | Discrete mathematics,Data structure,Model checking,Predicate abstraction,Abstract interpretation,Computer science,Skip list,Algorithm,Decidability,Theoretical computer science,Symbolic data analysis,Soundness | Conference |
Volume | ISSN | ISBN |
3855 | 0302-9743 | 3-540-31139-4 |
Citations | PageRank | References |
26 | 1.08 | 24 |
Authors | ||
7 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thomas Wies | 1 | 515 | 28.26 |
| Viktor Kuncak | 2 | 1129 | 70.57 |
| Patrick Lam | 3 | 636 | 38.73 |
| Andreas Podelski | 4 | 2760 | 197.87 |
| Martin C. Rinard | 5 | 4739 | 277.55 |
| e allen emerson | 6 | 7683 | 1183.13 |
| Kedar S. Namjoshi | 7 | 948 | 50.41 |