Bandera: The main goal of Bandera project is to integrate existing programming language processing methods with newly developed methods to provide automated support for the extraction of safe, compact, finite-state models which are suitable for verification from Java source code. While the ultimate goal is fully automated model extraction for a broad class of software systems, Bandera takes as a given that guidance from a software analyst may be required.
As illustrated in Figure above, the Bandera toolset is designed to be an open architecture in which a range of analysis and transformation components may be incorporated.