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

Using the BOOP Toolkit
After you have installed the BOOP Toolkit you are ready to use it. We provided a toy example (which is described in detail in the thesis). This example can be found in the example directory of the BOOP distribution.
The executable boop can be called with following parameters:
--reachable or -r Used to specify the name of the label
--verbose Increases the verbosity of BOOP: The report of the erroneous path contains more details and the theorem prover shows the expressions that it tries to decide.
--prosper-host Specifies the name of the host where the HOL98 theorem prover is running.
--prosper-port Specifies the number of the port on which the PROSPER Toolkit is listening.
--report Specify a file to which the counter example should be reported. If this parameter is missing, the counter example will be reported to stdout.
--iterations Specify a maximal number of interations.

Testing BOOP with an example program
You find an example program in the example directory of the BOOP distribution. The example is described in detail in the 3rd chapter of the master's thesis.
The code contains a few functions of a Linux device driver module. Linux device drivers are loaded and unloaded dynamically. The driver maintains a usage count, and it must not be released unless this count equals to zero.
We modified the interface functions so that the label ERROR is reachable if the driver is unloaded though the usage count is greater than zero.
Before you call boop, you must start the HOL98 theorem prover. You can do this by calling
start_hol &
	      
Then, call boop with following parameters:
boop -r ERROR example/spec.c example/driver.c
	      
If everything works, BOOP should report that ERROR is reachable. BOOP writes the intermediate abstractions to the actual directory, so you should find a number of files called abs<n>.[bp|exp]. On failure, it is a good idea to inspect these files.
BOOP provides a detailed explanation of how ERROR can be reached. If you edit the file driver.c, delete the line MOD_INC_USE_COUNT; and add it again after the instruction locked = TRUE; then ERROR should be unreachable.

Created by Georg Weißenbacher