On Verifying Complex Properties using Symbolic Shape Analysis

One of the main challenges in the verification of software systems is the analysis of statically unbounded data structures with dynamic memory allocation, such as linked data structures and arrays. We describe Bohne, a new analysis for verifying data structures. Bohne verifies data structure operations and shows that 1) the operations preserve data structure invariants and 2) the operations satisfy their specifications expressed in terms of changes to the set of objects stored in the data structure. During the analysis, Bohne infers loop invariants in the form of disjunctions of universally quantified Boolean combinations of formulas, represented as sets of binary decision diagrams. To synthesize loop invariants of this form, Bohne uses a combination of decision procedures for Monadic Second-Order Logic over trees, SMT-LIB decision procedures (currently CVC Lite), and an automated reasoner within the Isabelle interactive theorem prover. This architecture shows that synthesized loop invariants can serve as a useful communication mechanism between different decision procedures. In addition, Bohne uses field constraint analysis, a combination mechanism that enables the use of uninterpreted function symbols within formulas of Monadic Second-Order Logic over trees. Using Bohne, we have verified operations on data structures such as linked lists with iterators and back pointers, trees with and without parent pointers, two-level skip lists, array data structures, and sorted lists. We have deployed Bohne in the Hob and Jahob data structure analysis systems, enabling us to combine Bohne with analyses of data structure clients and apply it in the context of larger programs. This paper describes the Bohne algorithm, the techniques that Bohne uses to reduce the amount of annotations and the running time of the analysis. We also describe the analysis architecture that enables Bohne to effectively take advantage of multiple reasoning procedures when proving complex invariants.

Citation

Thomas Wies, Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard. On verifying complex properties using symbolic shape analysis. Technical Report MPI-I-2006-2-1, Max-Planck Institute for Computer Science, 2006.

BibTex Entry

@techreport{WiesETAL06VerifyingComplexPropertiesSymbolicShapeAnalysis,
  author = {Thomas Wies and Viktor Kuncak and Karen Zee and Andreas Podelski and Martin Rinard},
  title = {On Verifying Complex Properties using Symbolic Shape Analysis},
  institution = {Max-Planck Institute for Computer Science},
  year = 2006,
  number = {MPI-I-2006-2-1},
  url = {http://arxiv.org/abs/cs.PL/0609104},
  abstract = {
  One of the main challenges in the verification of software systems
  is the analysis of statically unbounded data structures with dynamic memory
  allocation, such as linked data structures and arrays.  We describe
  Bohne, a new analysis for verifying data structures.  Bohne verifies
  data structure operations and shows that 1) the operations preserve
  data structure invariants and 2) the operations satisfy their
  specifications expressed in terms of changes to the set of objects
  stored in the data structure.  During the analysis, Bohne infers
  loop invariants in the form of disjunctions of universally
  quantified Boolean combinations of formulas, represented as sets of
  binary decision diagrams.  To synthesize loop invariants of this
  form, Bohne uses a combination of decision procedures for Monadic
  Second-Order Logic over trees, SMT-LIB decision procedures
  (currently CVC Lite), and an automated reasoner within the Isabelle
  interactive theorem prover.  This architecture shows that
  synthesized loop invariants can serve as a useful communication
  mechanism between different decision procedures.  In addition, Bohne
  uses field constraint analysis, a combination mechanism that enables
  the use of uninterpreted function symbols within formulas of Monadic
  Second-Order Logic over trees.  Using Bohne, we have verified
  operations on data structures such as linked lists with iterators
  and back pointers, trees with and without parent pointers, two-level
  skip lists, array data structures, and sorted lists.  We have
  deployed Bohne in the Hob and Jahob data structure analysis systems,
  enabling us to combine Bohne with analyses of data structure clients
  and apply it in the context of larger programs.  This paper
  describes the Bohne algorithm, the techniques that Bohne uses
  to reduce the amount of annotations and the running time of the analysis.
  We also describe the analysis architecture that enables Bohne to 
  effectively take advantage of multiple reasoning procedures 
  when proving complex invariants.
}
}