An overview of the Jahob analysis system: Project Goals and Current Status

paper ps   
We present an overview of the Jahob system for modular analysis of data structure properties. Jahob uses a subset of Java as the implementation language and annotations with formulas in a subset of Isabelle as the specification language. It uses monadic second-order logic over trees to reason about reachability in linked data structures, the Isabelle theorem prover and Nelson-Oppen style theorem provers to reason about high-level properties and arrays, and a new technique to combine reasoning about constraints on uninterpreted function symbols with other decision procedures. It also incorporates new decision procedures for reasoning about sets with cardinality constraints. The system can infer loop invariants using new symbolic shape analysis. Initial results in the use of our system are promising; we are continuing to develop and evaluate it.

Citation

Viktor Kuncak and Martin Rinard. An overview of the Jahob analysis system: Project goals and current status. In NSF Next Generation Software Workshop, 2006.

BibTex Entry

@inproceedings{KuncakRinard06OverviewJahobAnalysisSystem,
  author = {Viktor Kuncak and Martin Rinard},
  title = {An overview of the {J}ahob analysis system: Project Goals and Current Status},
  booktitle = {{NSF} Next Generation Software Workshop},
  year = {2006},
  abstract = {
  We present an overview of the Jahob system for modular
  analysis of data structure properties.  Jahob uses a
  subset of Java as the implementation language and
  annotations with formulas in a subset of Isabelle as the
  specification language.  It uses monadic second-order
  logic over trees to reason about reachability in linked
  data structures, the Isabelle theorem prover and
  Nelson-Oppen style theorem provers to reason about
  high-level properties and arrays, and a new technique to
  combine reasoning about constraints on uninterpreted
  function symbols with other decision procedures. It also
  incorporates new decision procedures for reasoning about
  sets with cardinality constraints.  The system can infer
  loop invariants using new symbolic shape analysis.
  Initial results in the use of our system are promising; we
  are continuing to develop and evaluate it.
}
}