List of Figures

• Internal architecture of the Bandera Tool Set
• Bandera main window
• Main Frame and Session Manager Window
• Code Browse
• Error Trace
• Deadlock Sliced
• Pipeline Structure
• Methodology of property specification supported by Bandera
• Property Manager Window
• Abstraction Manager Window
• Pipeline Verified
• BSL organization
• BSL assertion syntax
• BSL predicate definition syntax
• BSL Pattern and Quantifier Syntax