Sciweavers

Share
IPPS
2006
IEEE

An overview of the Jahob analysis system: project goals and current status

10 years 5 months ago
An overview of the Jahob analysis system: project goals and current status
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 speciļ¬cation 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.
Viktor Kuncak, Martin C. Rinard
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where IPPS
Authors Viktor Kuncak, Martin C. Rinard
Comments (0)
books