Model Checking Software Using The Bogor Framework

Matthew B. Dwyer, John Hatcliff, and Robby
SAnToS Laboratory, Department of Computing and Information Sciences
Kansas State University

The Bogor Framework is a highly customizable and modular model checking framework aimed to ease the development of robust and efficient domain-specific model checkers for verification of dynamic and concurrent software. It provides a rich and extensible modeling language including features that allow for dynamic creation of objects and threads, garbage collection, dynamic dispatch of methods, and exception handling.

The extensible modeling language allows user-defined abstract data types and abstract operations as first class constructs. This is particularly useful when customizing Bogor to a particular family of software artifacts. Furthermore, its open modular design eases the task of customization to accomodate, for example, variations in scheduling policies, search modes for state exploration, state encodings, and checkers for specification languages.

Bogor employs state-of-the-art reduction techniques such as collapse compression, heap symmetry, thread symmetry, and partial-order reductions. Bogor has been successfully customized for ecient verification of realistic Java programs in the context of the Bandera project and real-time avionic systems in the context of the Cadena project.

The Bogor project site contains more information about Bogor including a freely available distribution, supporting documentation, related research papers and talks, and an example repository.

The tutorial will show how to customize Bogor to model check a particular family of software artifacts with examples drawn from standard Java libraries and avionic systems from Boeing.