The Bandera Tools for Model-checking Java Source Code:
A User's Manual

John Hatcliff and Oksana Tkachuk

March 7, 2001

• Contents
• List of Figures
• Introduction
• Overview
  • Challenges of model-checking program source code
  • When might someone be interested in learning about Bandera?
  • Architecture of Bandera
    • Java infrastructure and intermediate representation:
    • Java front-end:
    • Property specification:
    • Static analysis:
    • Approach to model construction:
    • Slicing:
    • Abstract interpretation:
    • Back end model generation:
• Installation
  • Requirements
  • Installing
    • UNIX
    • Windows 95/98/Me
    • Windows NT 4.0 or Windows 2000
  • Package Contents
  • Compiling
  • Running and The First Launch
• Overview of the Bandera User Interface
  • The Project and Code Panels
  • Sessions
  • Component Buttons
  • Session Manager
  • Property Specification Buttons
  • The PDG Browser
  • Abstract Type Inference
  • Pull-down Menus
• Guided Tour
  • UNIX or Linux
  • Windows
  • Simple Deadlock
  • Simple Deadlock with Slicing
  • Pipeline Example
    • The structure of the Pipeline example
    • Writing a specification using the Bandera Specification Language
    • Entering a specification using the Bandera User Interface
    • Using a simple data abstraction
  • Bounded Buffer Example
    • The structure of the Bounded Buffer example
    • Bounded Buffer requirements
    • Requirement one
    • Requirement two
    • Requirement three
    • Requirement four
    • Requirement five
    • Building a session for requirement one
    • Building a session for requirement three
    • A complete specification file
• The Bandera Specification Language
  • Introduction
  • Design Rationale
  • The Assertion Sublanguage
    • Rationale
    • Syntax and informal semantics
    • Implementation issues
  • The Temporal Specification Sublanguage
    • Predicate Definition Sublanguage
    • Syntax and informal semantics
    • Implicit Constraints
  • Specifying Temporal Patterns
    • Specifying Properties for Class Instances
    • Universal Class Instance Quantification
    • Implementation Issues
• The BUI Predicate Manager
• The BUI Pattern Manager
• The Bandera Slicer
  • Appropriate notions of dependence for concurrent Java
  • How slicing criteria are generated
  • Using the dependency browser
• The Bandera Abstraction Tools
• Limitations and Known Bugs
• References
• About this document ...