Combining Theorem proving with Static Analysis for Data Structure Consistency

paper ps   
We describe an approach for combining theorem proving techniques with static analysis to analyze data structure consistency for programs that manipulate heterogeneous data structures. Our system uses interactive theorem proving and shape analysis to verify that data structure implementations conform to set interfaces. A simpler static analysis then uses the verified set interfaces to verify properties that characterize how shared objects participate in multiple data structures. We have successfully applied this technique to several programs and found that theorem proving within circumscribed regions of the program combined with static analysis enables the verification of large-scale program properties.

Citation

Karen Zee, Patrick Lam, Viktor Kuncak, and Martin Rinard. Combining theorem proving with static analysis for data structure consistency. In International Workshop on Software Verification and Validation, Seattle, November 2004.

BibTex Entry

@inproceedings{ZeeETAL04CombiningTheoremStaticAnalysisDataStructureConsistency,
  author = {Karen Zee and Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {Combining Theorem proving with Static Analysis for Data Structure Consistency},
  booktitle = {International Workshop on Software Verification and Validation},
  year = 2004,
  address = {Seattle},
  month = {November},
  abstract = {
We describe an approach for combining theorem proving
techniques with static analysis to analyze data structure
consistency for programs that manipulate heterogeneous data
structures.  Our system uses interactive theorem proving and
shape analysis to verify that data structure implementations
conform to set interfaces.  A simpler static analysis then
uses the verified set interfaces to verify properties that
characterize how shared objects participate in multiple data
structures.  We have successfully applied this technique to
several programs and found that theorem proving within
circumscribed regions of the program combined with static
analysis enables the verification of large-scale program
properties.
}
}