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

Installing the BOOP Toolkit (2)
Make sure that you have already installed HOL98, the PROSPER Toolkit and the MOPED model checker! The instructions for installing these tools can be found here.

Installing GCC 3.2 and the BOOP Toolkit v0.42
The BOOP source tarball contains three directories:
ast The source code that wraps the GNU C compiler 3.2. It contains the "Abstract Syntax Tree" module.
bop The source files for abstraction and refinment, and the sources for interfacing to HOL98 and MOPED. This is the main package.
example A simple example that can be used to test BOOP after it has been installed. The example is described in detail in the thesis.

Unpack the BOOP source tarball into a subdirectory in your home directory:
tar xzvf boop-0.42.tar.gz
              
Before you can compile the BOOP Toolkit, you need to unpack the sources of the GNU C compiler, too. During the build of the BOOP Toolkit a symbolic link to the ast directory will be added to the source tree of GCC 3.2 (in the subdirectory gcc). The installation guide for GCC 3.2 recommends that GCC should not be built in its source directory!

Configuring the BOOP sources
After you have unpacked the BOOP source tarball and the GCC 3.2 sources, you have to configure the BOOP Makefile. Enter the bop directory and call
configure --bindir=<binary directory>
          GCCSRCDIR=<GCC sources>
          GCCOBJDIR=<GCC build dir>
              
The paths that you specify must be absolute paths! The binary directory is the directory where the binaries will be installed after you have built BOOP. The GCC sources path specifies the directory to which you have unpacked the GCC sources. The GCC build dir specifies the directory where GCC will be built; This directory is created during the build if it does not exist.

Building the BOOP Toolkit
After you have configured the BOOP sources, there should be a file called Makefile in the bop directory. You can now call
make
              
to start building the BOOP Toolkit. The build will take a while, since the GCC sources are rather large. If the build is successful, there should be a file called boop in the bop directory.

Installing the BOOP Toolkit
You can now install the BOOP binaries in the directory you have specified by calling
make install
              
This installs the executables boop, bopCallMoped.pl, and start_hol. Add the directory where these binaries reside to your path, since boop calls bopCallMoped.pl and can only find it if it is in the search path.

Testing and Using the BOOP Toolkit
After you have installed the BOOP Toolkit you should test it with the toy example that we provided. You find an explanation of how this can be accomplished here.
Created by Georg Weißenbacher