Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-2006-2-001

On verifying complex properties using symbolic shape analysis

Wies, Thomas and Kuncak, Viktor and Zee, Karen and Podelski, Andreas and Rinard, Martin

MPI-I-2006-2-001. April 2006, 32 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
One of the main challenges in the verification of software systems
is the analysis of 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 report
describes the Bohne algorithm as well as techniques that Bohne uses
to reduce the ammount of annotations and the running time of the analysis.

Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-2006-2-001.ps377 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2006-2-001
Hide details for BibTeXBibTeX
@TECHREPORT{WiesKuncakZeePodelskiRinard2006,
  AUTHOR = {Wies, Thomas and Kuncak, Viktor and Zee, Karen and Podelski, Andreas and Rinard, Martin},
  TITLE = {On verifying complex properties using symbolic shape analysis},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2006-2-001},
  MONTH = {April},
  YEAR = {2006},
  ISSN = {0946-011X},
}