Implications of a Data Structure Consistency Checking System

paper ps   
We present a framework for verifying that programs correctly preserve important data structure consistency properties. Results from our implemented system indicate that our system can effectively enable the scalable verification of very precise data structure consistency properties within complete programs. Our system treats both internal properties, which deal with a single data structure implementation, and external properties, which deal with properties that involve multiple data structures. A key aspect of our system is that it enables multiple analysis and verification packages to productively interoperate to analyze a single program. In particular, it supports the targeted use of very precise, unscalable analyses in the context of a larger analysis and verification system. The integration of different analyses in our system is based on a common set-based specification language: precise analyses verify that data structures conform to set specifications, whereas scalable analyses verify relationships between data structures and preconditions of data structure operations. There are several reasons why our system may be of interest in a broader program analysis and verification effort. First, it can ensure that the program satisfies important data structure consistency properties, which is an important goal in and of itself. Second, it can provide information that insulates other analysis and verification tools from having to deal directly with pointers and data structure implementations, thereby enabling these tools to focus on the key properties that they are designed to analyze. Finally, we expect other developers to be able to leverage its basic structuring concepts to enable the scalable verification of other program safety and correctness properties.

Citation

Viktor Kuncak, Patrick Lam, Karen Zee, and Martin Rinard. Implications of a data structure consistency checking system. In International conference on Verified Software: Theories, Tools, Experiments (VSTTE, IFIP Working Group 2.3 Conference), Zürich, Switzerland, October 2005.

BibTex Entry

@inproceedings{KuncakETAL05ImplicationsDataStructureConsistencyCheckingSystem,
  author = {Viktor Kuncak and Patrick Lam and Karen Zee and Martin Rinard},
  title = {Implications of a Data Structure Consistency Checking System},
  booktitle = {International conference on Verified Software: Theories, Tools, Experiments (VSTTE, IFIP Working Group 2.3 Conference)},
  year = 2005,
  address = {Z\"urich, Switzerland},
  month = {October},
  abstract = {
We present a framework for verifying that programs correctly preserve
important data structure consistency properties. Results from our
implemented system indicate that our system can effectively enable the
scalable verification of very precise data structure consistency
properties within complete programs. Our system treats both {\em
internal} properties, which deal with a single data structure
implementation, and {\em external} properties, which deal with
properties that involve multiple data structures. A key aspect of our
system is that it enables multiple analysis and verification packages
to productively interoperate to analyze a single program.  In
particular, it supports the targeted use of very precise, unscalable
analyses in the context of a larger analysis and verification system.
The integration of different analyses in our system is based
on a common set-based specification language: precise
analyses verify that data structures conform to set
specifications, whereas scalable analyses verify relationships
between data structures and preconditions of data structure
operations.

There are several reasons why our system may be of interest in a broader
program analysis and verification effort. First, it can ensure that
the program satisfies important data structure consistency properties,
which is an important goal in and of itself.  Second, it can provide
information that insulates other analysis and verification tools from
having to deal directly with pointers and data structure
implementations, thereby enabling these tools to focus on the key
properties that they are designed to analyze. Finally, we expect other
developers to be able to leverage its basic structuring concepts to
enable the scalable verification of other program safety and
correctness properties.
}
}