Bandera is a tool for automatically extracting finite-state models from Java source code. It addresses the challenges of constructing finite-state models for software verification, which is often hindered by the semantic gap between software development and verification tools. Bandera uses a component-based architecture to provide automated support for model extraction, including slicing, abstraction, and specialization. It allows users to specify properties in temporal logic and generates models in the input language of verification tools. Bandera also maps verification results back to the original source code, enabling error analysis. The tool includes a graphical user interface for interacting with the model extraction process and displaying counterexamples. Bandera's architecture is similar to an optimizing compiler, using intermediate representations to stage transformations. It supports various verification tools and provides a flexible framework for extending its capabilities. Bandera has been applied to check properties of Java programs, demonstrating its effectiveness in reducing model size and improving verification efficiency. The tool is designed to be extensible and supports a range of analyses to enhance model precision and compactness. Bandera's approach enables the application of finite-state verification techniques to software, overcoming the challenges of model construction and state explosion. The tool has been used to verify properties of multi-threaded Java programs, showing its potential for scalable verification. Bandera's design allows for the integration of new analysis techniques and verification tools, making it a valuable resource for software verification.Bandera is a tool for automatically extracting finite-state models from Java source code. It addresses the challenges of constructing finite-state models for software verification, which is often hindered by the semantic gap between software development and verification tools. Bandera uses a component-based architecture to provide automated support for model extraction, including slicing, abstraction, and specialization. It allows users to specify properties in temporal logic and generates models in the input language of verification tools. Bandera also maps verification results back to the original source code, enabling error analysis. The tool includes a graphical user interface for interacting with the model extraction process and displaying counterexamples. Bandera's architecture is similar to an optimizing compiler, using intermediate representations to stage transformations. It supports various verification tools and provides a flexible framework for extending its capabilities. Bandera has been applied to check properties of Java programs, demonstrating its effectiveness in reducing model size and improving verification efficiency. The tool is designed to be extensible and supports a range of analyses to enhance model precision and compactness. Bandera's approach enables the application of finite-state verification techniques to software, overcoming the challenges of model construction and state explosion. The tool has been used to verify properties of multi-threaded Java programs, showing its potential for scalable verification. Bandera's design allows for the integration of new analysis techniques and verification tools, making it a valuable resource for software verification.