Title: 
  Bandera : Extracting Finite-state Models from Java Source Code

Speaker:
  Matthew Dwyer
  Kansas State University

Abstract:

Model checkers and other finite-state verification tools allow
developers to detect certain kinds of errors automatically.
Despite the successful application of these techniques to reasoning about
hardware systems, their application to software systems has been slow.  
While there are several obstacles to adoption of these methods
by software developers, we believe the most significant of these to be
the need for translation of programs written in high-level languages
to the low-level input languages of verification tools.
This translation must be automated to insure correctness and
furthermore it must be optimized to construct the smallest
possible model in order to mitigate the significant computational
complexity of finite-state verification.
The Bandera toolset does precisely this for programs written in Java.

Bandera combines well-established programming language
analysis and transformation techniques, such as program
slicing, control-flow analysis, abstract interpretation,
and partial evaluation, to extract a compact transition
system representation of the input program.  The semantics-preserving
nature of these techniques insures that for an input program
and property the soundness of model checking on the extracted
transition system is preserved.
In this talk, we describe the design of Bandera and give 
several examples of its application.