Main Menu

• Home
• Team
  • Robby, Faculty, Project Leader
  • Matthew B. Dwyer, Faculty
  • John Hatcliff, Faculty
  • Matthew Hoosier, (Past) Full-time Developer
• Downloads
• Papers
  • Kiasan/KUnit: Automatic Test Case Generation and Analysis Feedback for Open Object-oriented Systems
  • Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Orient
  • Enabling Efficient Partial Order Reductions for Model Checking Object-oriented Programs
  • Building Your Own Software Model Checker Using The Bogor Extensible Model Checking Framework
  • Bogor: An Extensible Framework for Domain-Specific Model Checking
  • Supporting Model Checking Education using BOGOR/Eclipse
  • A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checkin
  • Space-Reduction Strategies for Model Checking Dynamic Systems
  • Bogor: Flexible Framework for Creating Software Model Checkers
  • Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems
  • Using Design Metrics for Predicting System Flexibility
  • Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs
  • Extending JML for Modular Specification and Verification of Multi-Threaded Programs
  • A Case Study in Domain-customized Model Checking for Real-time Component Software
  • Analyzing Interaction Orderings with Model Checking
  • Checking Strong Specifications Using An Extensible Software Model Checking Framework
  • Verifying Atomicity Specifications for Concurrent Object-Oriented Software using Model Checking
  • Space Reductions for Model Checking Quasi-Cyclic Systems
  • Bogor: An Extensible and Highly-Modular Model Checking Framework
  • Model-checking Middleware-based Event-driven Real-time Embedded Software
  • Exploiting Object Escape and Locking Information in Partial Order Reduction for Concurrent Object-Or
  • Checking JML Specifications Using An Extensible Software Model Checking Framework
• Documentation
  • Getting Started
    • About Bogor
    • Downloading Bogor
    • Running Bogor
    • Bogor Architecture
    • Setting Up Eclipse for Bogor Extension Development
  • Bogor Input Representation (BIR)
    • BIR Specification
    • BIR Concrete Syntax
  • Language Extensions
    • Set Extension - A Walkthrough
    • Wrapper Extension
  • Miscellaneus Modules/Framework
    • Event Framework
  • Domain Customizations
    • BogorVM: Customizing Bogor for model checking Java programs
  • Tips and Tricks
    • Compiling and Deploying Bogor
    • Contributing A Bogor Documentation
• API 
• Examples
  • High-level BIR Examples
    • DinnerDate Example
  • Low-level BIR Examples
    • DinnerDate Example
    • nDiningPhilosophers Example
    • SumToN Example
    • ReadersWriters Example
    • NWorkers Example
  • Java (Automatically) Translated Examples
    • Deadlock (Bandera)
    • BoundedBuffer (BogorVM)
    • Deadlock (BogorVM)
  • Java (Manually) Translated Examples
    • BoundedBuffer
    • Deadlock
• Repository 
• Bug Reports 
• Licenses
• Forums 
• Bogor Users Map 
• Site Map
• Contact Us
• Search

• Administrator