The BOOP Toolkit

Developed at the
Institute for Software Technology

The BOOP Toolkit
This page contains all information that you need for downloading, installing and using the BOOP Toolkit.
About BOOP
Downloading BOOP
Installing BOOP
Using BOOP
Documentation (Thesis)
Reporting problems

Links
The BOOP Toolkit was not implemented from the scratch. We utilized the tools of several other research groups. Please visit the homepages of the following projects, too:
HOL98 Theorem Prover
Moscow ML 2.0
The PROSPER Toolkit
MOPED
GCC 3.2
Microsoft SLAM project

Download tarballs
Download the tarballs that are necessary to install the BOOP Toolkit!
HOL98 Taupo 6
Moscow ML 2.01
PROSPER v1.4
MOPED
CUDD Library
SPIN model checker
GCC 3.2 sources
BOOP v0.42

SourceForge.net Logo

About the BOOP Toolkit
The BOOP Toolkit was implemented within the scope of the master's thesis of Georg Weißenbacher at the Institute for Software Technology at Graz University of Technology. It is based on the SLAM project of Microsoft Research. The BOOP Toolkit uses abstraction and refinement to determine the reachability of program points in a C program. When the BOOP Toolkit is applied on a C program, it repeatedly passes through three phases:
  • Abstraction: We apply theorem proving and predicate transformers to remove detail from a C program.
  • Model Checking: A model checker is applied on the abstract program to search for erroneous execution traces (with respect to a specification that must be provided by the user).
  • Refinement: If the model checker found an error path which is feasible in the original C program, it is reported to the user. If the path is infeasable, the abstraction is refined by adding more detail and the process is reiterated.

News
Georg is now an associate professor in the FORSYTE group of TU Wien. He was previously a postdoctoral research associate at Princeton University, after graduating with a doctoral degree from Oxford University.
We have implemented a nice heuristic to handle programs with deep loops in SATABS. Check out our loop detection benchmarks and our CAV'06 paper "Counterexamples with Loops for Predicate Abstraction".
The installation instructions were updated after Flora Amato and Andreas Polzer reported some problems with HOL98. Please note that BOOP isn't actively maintainted anymore. If you want to use an abstraction/refinement framework for your research, I would recommend to use my new tool Wolverine. The SLAM-based Static Driver Verifier is distributed as part of the Windows Driver Foundation and is now an industry-strength verification tool.

Project members
The BOOP Toolkit was implemented by Georg Weißenbacher as partly fulfillment of his master's thesis. The thesis was written at the Institute for Software Technology at Graz University of Technology. It was supervised by Roderick Bloem.
Georg Weißenbacher weissenb(at)forsyte.at
Roderick Bloem rbloem(at)iaik.tugraz.at

Related work
The SLAM project The SLAM project is conducted by Tom Ball and Sriram K. Rajamani at Microsoft Research. The BOOP Toolkit is basically a reimplementation of the C2BP and Newton tool that are part of the SLAM Toolkit.
The BLAST Toolkit The BLAST Toolkit pursues a similar abstraction/refinement approach to check that software satisfies behavioral properties of the interfaces it uses. It uses lazy abstraction, i.e. it does not recalculate the complete abstract program in each iteration step.
SATABS SATABS is an abstraction verification framework that is based on SAT solving. It was developed by Daniel Kröning at CMU and is actively improved by him and his group at ETH Zurich.
Java Pathfinder Java Pathfinder is a tool that was developed by the Automated Software Engineering group at NASA Ames. It is a verification and testing environment for Java which integrates model checking, program analysis and testing.
MOPED The MOPED model checker is a model checker for Boolean programs and pushdown automata. It is integrated into the BOOP Toolkit and can be used together with the SLAM Toolkit.

Created by Georg Weißenbacher