Bogor (Robby, Dwyer, and Hatcliff 2006) is an extensible software model-checking framework which includes:
- Software model checking algorithms
- Visualizations
- A user interface designed to support both general-purpose and domain-specific software model checking
Bogor provides support for object-oriented features such as dynamic creation of threads and objects, object inheritance, virtual methods, exceptions, and garbage collection. Bogor can be extended with new modeling types, expressions, and commands, new algorithms (e.g., for state-space exploration, state storage, etc) and new optimizations (e.g., heuristic search strategies, domain-specific scheduling, etc.).