These pages present the Bandera tool set for model checking concurrent Java software. The next generation of the Bandera tool set is under development and we hope to have an initial public release ready by the summer of 2005. The next generation of Bandera will provide significantly more robust and scalable software checking capabilities than those found in Bandera 0.3 (the latest version described on these web pages).

You may also be interested in looking at some other software tools that have been developed in the SAnToS Group at Kansas State University and the ESQuaReD Group at University of Nebraska (Lincoln).

• Bogor -- an Eclipse Ready extensible and customizable model checking engine for object-oriented software. Bogor provides direct support for many OO language features including dynamically created objects and threads, inheritance, exceptions, garbage collection. In addition, Bogor's extension facilities allow new commands and data types to be added to its modeling language. Bogor is the core model checking engine of the next generation of Bandera.
• Cadena -- a sophisticated Eclipse-based IDE for specification, analysis, and development of distributed systems built using the CORBA Component Model (CCM). Cadena is being used by research engineers at several companies including Boeing and Lockheed Martin to investigate the capabilities of model driven development for avionics and command and control systems.
• Indus -- is a collection of static analysis and program transformation libraries for Java. One the current emphases of Indus is a robust program slicing capability for full Java. Kaveri is an Eclipse-based user interface for the Indus slicer that provides a number of capabilities for computing program slices and navigating and querying program dependence graphs.
• JML Eclipse -- is an Eclipse front end for JML tools that provide verification and analysis capabilities for Java program specifications written in the Java Modeling Language (JML). JML is a sophisticated behavioral interface specification language that provides a variety of useful constructs for specifying Java assertions, pre/post-conditions, class invariants, and light-weight semantic constraints.

Finite-state verification techniques, such as model checking, are attractive because they are capable of exposing very subtle defects in the logic of sequential and concurrent systems. Tool support for these techniques has reached a level of maturity where the hardware and telecommunications industries are beginning to incorporate them as a component of their development processes. Applying those tools to software system validation is not as easy for a variety of reasons.

The Bandera project addresses one of the major obstacles in the path of practical finite-state verification of software. Tools like SMV and SPIN accept a description of a finite-state transition system as input. Bridging the semantic gap between a non-finite-state software system expressed as source code and those tool input languages requires the application of sophisticated program analysis, abstraction, and transformation techniques.

The goal of the Bandera project is to integrate existing programming language processing techniques with newly developed techniques to provide automated support for the extraction of safe, compact, finite-state models that are suitable for verification from Java source code. While our ultimate goal is fully-automated model extraction for a broad class of software systems, our approach takes as a given that guidance from a software analyst may be required.

The Bandera toolset is designed to be an open architecture in which a variety of analysis and transformation components may be incorporated.

If you are interested in papers that give an overview of Bandera, we recommend the following three. The first gives an overview of the Bandera tools. The second describes the current user interface of Bandera, and presents the methodology that users are intended to follow. The third gives a detailed presentation of Bandera's temporal specification language.

• Bandera: Extracting Finite-state Models from Java Source Code, James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, Hongjun Zheng in Proceedings of the 22nd International Conference on Software Engineering, June, 2000.
• Using the Bandera Tool Set to Model-check Properties of Concurrent Java Software, June, 2001. John Hatcliff and Matthew Dwyer To appear in the Proceedings of CONCUR 2001. (invited tutorial paper)
• Expressing Checkable Properties of Dynamic Systems: The Bandera Specification Language, June, 2001. James Corbett, Matthew Dwyer, John Hatcliff, Robby KSU CIS Technical Report 2001-04. (Submitted for journal publication; this paper is an extended version of our 2000 Spin Workshop paper)