In this talk, we describe Bandera -- an integrated collection of tools for model-checking concurrent Java software that attempts to overcome the obstacles described above. Bandera is a model compiler in the sense that it takes Java source code as input and compiles it to a program model expressed in the input language of one of several existing verification tools including SMV, Spin, dSpin, and JPF. Program slicing and abstract interpretation components are used during compilation to customize the program model with respect to the properties being checked. Bandera is like a debugger in the sense that it maps counterexamples produced by back-end model checkers back to the source code level, and it allows the user to replay program execution both forwards and backwards along the path of the counterexample.
We illustrate the functionality of Bandera's major components with a demo of the tool on several examples. This will include an overview of how Bandera's extensible temporal property specification language can be used to specify temporal properties in terms of Java source code features. We summarize results of using Bandera to verify properties of safety-critical software including avionics applications. We conclude with a discussion of other forms of automated tool support that we are currently working on that we believe will be necessary for model-checking properties of large code bases.