The Bandera
toolset provides a means for automatic generation
of formal models and verification of Java programs. Bandera is
an integrated collection of code analysis, transformation, and
verification components and tools. Bandera takes as input a Java
source code, a temporal specification to be verified, and some
level of abstraction guidance from user. It then uses slicing and
abstraction techniques to transform the code and generate a program
model in the input language of an existing verifier, like SPIN or
SMV. The output of the verifier can be mapped back to the Java
source code.
In this talk I will present a brief overview of model checking
technique and the challenges involved. I will then present how Bandera
addresses these challenges and explain the function of key components
of the tool. I will show how Bandera can be used by presenting
examples during the talk.