"I verify, therefore I am consistent!"

hob. 1. The block in the center of a wheel, from which the spokes radiate, and through which the axle passes; -- called also hub or hob.

Webster's Revised Unabridged Dictionary, © 1996, 1998 MICRA, Inc.

Diagram Highlighting Our Approach

The goal of the Hob project is to verify sophisticated properties of programs that manipulate complex, heterogenous data structures.

News

Overview

Our technique enables the verification of data structure consistency constraints by applying multiple analyses to different modules in the same program. In our approach, each module encapsulates one or more data structures and uses membership in abstract sets to characterize how objects participate in data structures. Each analysis verifies that the implementation of the module 1) preserves important internal data structure consistency properties and 2) correctly implements an interface that uses formulas in a set algebra to characterize the effects of operations on the encapsulated data structures. Collectively, the analyses use the set algebra to 1) characterize how objects participate in multiple data structures and to 2) enable the inter-analysis communication required to verify properties that depend on multiple modules analyzed by different analyses.

We have implemented our system and deployed three pluggable analyses into it: a flag analysis for modules in which abstract set membership is determined by a flag field in each object, a plugin for modules that encapsulate linked data structures such as lists and trees, and an array plugin in which abstract set membership is determined by membership in an array. Our experimental results indicate that our approach makes it possible to effectively combine multiple analyses to verify properties that involve objects shared by multiple modules, with each analysis analyzing only those modules for which it is appropriate.

Implementation

Our implementation provides an infrastructure with several general components that perform tasks required by all analyses. The implementation language component can parse and type-check implementation sections. It produces an abstract syntax tree and methods that allow analyses to conveniently access this representation. Similarly, the specification component can parse and type check specification sections and provides access to the resulting abstract syntax tree. Large parts of abstraction sections are expressed in a language that is specific to each analysis. The abstraction section component parses those parts of the abstraction section syntax that are common to all analyses and uses uninterpreted strings to pass along the analysis-specific parts. Finally, the implementation provides a driver that processes the program and invokes the appropriate analysis for each module that it encounters. Our implementation consists of approximately 10,000 lines of O'Caml code, to which the flag plugin contributes 2000 lines, the PALE plugin another 700 lines, and the array analysis plugin 1000 lines.

Software

Papers (see also homepages of project members):

Presentations

People

Last modified by plam, on Thu Oct 28 14:13:04 EDT 2004.

Valid XHTML 1.0! Valid CSS!