Bogor Website

About Bogor

Bogor is an extensible software model checking framework with state of the art software model checking algorithms, visualizations, and user interface designed to support both general purpose and domain-specific software model checking. Although there are many model checkers available, Bogor provides a number novel capabilities that make it especially well-suited for checking properties of a variety modern software artifacts, for building your own domain-specific engine, and for using it to teach model checking concepts.

Direct support of features found concurrent object-oriented languages such as dynamic creation of threads and objects, object inheritance, virtual methods, exceptions, garbage collection, etc.
Bogor's modeling language can be extended with new primitive types, expressions, and commands associated with a particular domain (e.g, multi-agent systems, avionics, security protocols, etc.) and a particular level of abstraction (e.g., design models, source code, byte code, etc.).
Bogor's open architecture well-organized module facility allows new algorithms (e.g., for state-space exploration, state storage, etc) and new optimizations (e.g., heuristic search strategies, domain-specific scheduling, etc.) to be easily swapped in to replace Bogor's default model checking algorithms.
Bogor has a robust feature-rich graphical interface implemented as a plug-in for Eclipse -- an open source and extensible universal tool platform from IBM. This user interface provides mechanisms for collecting and naming different Bogor configurations, specification property collections, and a variety of visualization and navigation facilities.
Bogor is an excellent pedagogical vehicle for teaching foundations and applications of model checking because it allows students to see clean implementations of basic model checking algorithms and to easily enhance and extend these algorithms in course projects (read more and see available course materials).

In short, Bogor aims to be not only a robust and feature-rich software model checking tool that handles the language constructs found in modern large-scale software system designs and implementations, it also aims to be a model checking framework that enables researchers and engineers to create families of domain-specific model checking engines.
Read more...

You may also be interested in looking at some other software tools that have been developed in the SAnToS Group at Kansas State University and the ESQuaReD Group at University of Nebraska (Lincoln).

Bandera -- a toolset for model checking concurrent Java programs. The next generation of Bandera is being actively developed and it will support a large subset of Java and its standard library, JML, and an IDE built on top of Eclipse.
Cadena -- a sophisticated Eclipse-based IDE for specification, analysis, and development of distributed systems built using the CORBA Component Model (CCM). Cadena is being used by research engineers at several companies including Boeing and Lockheed Martin to investigate the capabilities of model driven development for avionics and command and control systems.
Indus -- is a collection of static analysis and program transformation libraries for Java. One of the current emphases of Indus is a robust program slicing capability for full Java. Kaveri is an Eclipse-based user interface for the Indus slicer that provides a number of capabilities for computing program slices and navigating and querying program dependence graphs.
JML Eclipse -- is an Eclipse front end for JML tools that provide verification and analysis capabilities for Java program specifications written in the Java Modeling Language (JML). JML is a sophisticated behavioral interface specification language that provides a variety of useful constructs for specifying Java assertions, pre/post-conditions, class invariants, and light-weight semantic constraints.