Finite-state verification techniques, such as model checking, have
shown promise as a cost-effective means for finding defects in
hardware designs. To date, the application of these techniques to
software has been hindered by several obstacles. Chief among these is
the problem of constructing a finite-state model that approximates the
executable behavior of the software system of interest. Current
best-practice involves hand-construction of models which is expensive
(prohibitive for all but the smallest systems), prone to errors (which
can result in misleading verification results), and difficult to
optimize (which is necessary to combat the exponential complexity of
verification algorithms).
In this talk, we describe an integrated collection of program
analysis and transformation components, called Bandera, that enables
the automatic extraction of safe, compact finite-state models from
program source code. Bandera takes as input Java source code and
generates a program model in the input language of one of several
existing verification tools; Bandera also maps verifier outputs back
to the original source code. We discuss the major components of
Bandera and give an demonstration of how it can be used to model check
correctness properties of Java programs.
Last modified: Mon Apr 17 14:34:22 MET DST 2000