The paper introduces Bandera, a tool designed to extract finite-state models from Java source code for model checking. Bandera addresses the challenges of constructing finite-state models for software systems, which are often more complex and harder to handle than those for hardware designs. The tool uses a component-based architecture that includes slicing, abstract interpretation, and specialization to automate the model extraction process. Bandera also supports the mapping of verifier outputs back to the original source code, facilitating error trace interpretation. The paper discusses the design and implementation of Bandera, its integration with existing verification tools, and its application to a multi-threaded Java program. The results demonstrate the effectiveness of Bandera in reducing the state space and improving the scalability of model checking for software systems.The paper introduces Bandera, a tool designed to extract finite-state models from Java source code for model checking. Bandera addresses the challenges of constructing finite-state models for software systems, which are often more complex and harder to handle than those for hardware designs. The tool uses a component-based architecture that includes slicing, abstract interpretation, and specialization to automate the model extraction process. Bandera also supports the mapping of verifier outputs back to the original source code, facilitating error trace interpretation. The paper discusses the design and implementation of Bandera, its integration with existing verification tools, and its application to a multi-threaded Java program. The results demonstrate the effectiveness of Bandera in reducing the state space and improving the scalability of model checking for software systems.