Overview

Ensuring data structure consistency is important for constructing reliable software systems. With the advances of modern memory-safe programming languages that eliminate low-level errors, high-level data structure consistency properties will become one of the main sources of errors in programs.

The goal of Project Jahob is to demonstrate that it is possible to statically verify complex data structure consistency properties in non-trivial programs. To achieve this goal, Jahob combines techniques from static analysis (such as shape analysis), decision procedures and theorem proving.

Jahob can be viewed as a static analysis and verification system for modular analysis of imperative computer programs that manipulate relations as state components. In Jahob, relations are either 1) directly given in terms of the programming language constructs such as object fields, or 2) implemented using container data structures in terms of other primitives. Jahob addresses both 1) the problem of analyzing constraints on (concrete and abstract) relations, and 2) the problem of verifying that data structures correctly implement the abstract relations.

The input language for Jahob is a subset of Java extended with annotations written as special comments. Therefore, Jahob programs can be 1) compiled and executed using existing Java compilers and virtual machines, and 2) statically verified to satisfy important data structure consistency properties.

Background

The predecessor of project Jahob is the Hob project. Hob demonstrated the effectiveness of using data refinement as a technique for combining heterogeneous analyses in the same program by applying different analyses to different program modules. Unlike Hob, Jahob starts with a subset of Java as the input language. The goal of Jahob is to experiment with several features that go beyond Hob: a more general specification language that includes relations, the specification of instantiatable data structures, and the combination of reasoning techniques not only at the level of modules, but also at the level of procedures, individual statements, and verification conditions.

Current Status

We have used Jahob to evaluate a decision procedure for sets with cardinality constraints. We are in the process of developing example applications with Jahob, developing a methodology for using data abstraction, developing techniques for loop invariant inference, and developing specialized analyses for relations and pointer structures.

More Information

More information about Project Jahob is available from http://www.cag.csail.mit.edu/~vkuncak/projects/jahob/index.html.

Research Support

This research was supported in part by DARPA Contract F33615-00-C-1692, NSF Grant CCROO-86154, NSF Grant CCROO-63513, and the Singapore-MIT Alliance.

References:

[1] Viktor Kuncak and Martin Rinard. The First-Order Theory of Sets with Cardinality Constraints is Decidable. MIT CSAIL Technical Report 958, July 2004.

[2] Viktor Kuncak and Martin Rinard. Decision Procedures for Set-Valued Fields. In 1st International Workshop on Abstract Interpretation of Object-Oriented Languages, Paris, France, January 2005.

[3] Patrick Lam, Viktor Kuncak, and Martin Rinard. Hob: A Tool for Verifying Data Structure Consistency. In 14th International Conference on Compiler Construction (tool demo), Edinburgh, Scotland, April 2005.

[4] 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 (SVV 2004). Seattle, November 2004.