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

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
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
CUDD Library
SPIN model checker
GCC 3.2 sources
BOOP v0.42 Logo

BOOP depends on several tools that have changed in the last year, so you might run into problems even if you follow the installation instructions thoroughly. Since the BOOP toolkit isn't maintained anymore, you might want to consider using other tools like BLAST or SLAM.
Installing the BOOP Toolkit (1)
Before you try to install the BOOP Toolkit v0.42 make sure that you have downloaded the following files from our download area:
  • boop-0.42.tar.gz
  • taupo-6.tar.gz
  • mos20src.tar.gz
  • prosper1-4.tar.gz
  • moped-021007-src.tar.gz
  • cudd-2.3.1.tar.gz
  • spin402.tar.gz
  • gcc-3.2.tar.gz
Each of these packages comes with detailed installation instructions. Please follow them carefully! We recommend to install the programs in the following order:
  1. HOL98 Theorem Prover
  2. PROSPER Toolkit
  3. MOPED model checker
  4. GCC 3.2 sources
  5. BOOP Toolkit
BOOP has been developed for PC's running the Linux operating system, but it will probably run on most Unix systems.
We provide some hints for the installation of HOL98, PROSPER, MOPED and GCC:

Hints for installing HOL98
You have to use HOL98 Taupo 6. BOOP won't work with the newer HOL4 because the PROSPER Toolkit doesn't! Follow the installation instructions carefully. You will have to install Moscow ML 2.0 before you can install HOL98. Be sure to download the source files of Moscow ML 2.01! When you compile Moscow ML you must build the sockets library. The instructions are located in the Moscow ML distribution in the directory src/dynlibs/msocket/README.
Note, that HOL98 Taupo 6 and Kananaskis-1 no longer build successfully because of the so called overflow bug, caused by the fact that more than 231 seconds have passed since 1 January 1970. In the file src/portableML/Portable.sml, replace the local-in-end block that defines mk_time, dest_time and some others with
  local open Time
        val two_30 = Math.pow(2.0, 30.0)
    val timestamp : unit -> time = now
    val time_to_string : 
      time -> string = toString
    fun dest_time t = 
      let val adjusted = 
            Real.-(toReal t, two_30)
          val sec = Real.trunc adjusted
        {sec=sec, usec=0}
    fun mk_time {sec,usec} = 
      fromReal (Real.+(real sec, two_30))
    fun time_eq (t1:time) t2 = (t1 = t2)
    fun time_lt (t1:time) t2 = Time.<(t1,t2)
More hints can be found in the FAQ section of the HOL Sourceforge page. I want to thank Flora Amato and Andreas Polzer for reporting this problem as well as the solution.
Hints for installing PROSPER 1.4
Before you install the PROSPER Toolkit you must have installed HOL98. We recommend to install PROSPER in your home directory, since you need write access to the PROSPER directory when you compile the BOOP Toolkit. During the installation you have to set the environment variables PROSPER and HOLDIR. Make sure that this variables are set when you configure the BOOP Toolkit, because otherwise BOOP cannot find the PROSPER directory! $HOLDIR/bin must contain Holmake!
Hints for installing MOPED
Moped requires Fabio Somenzi's BDD library CUDD and the SPIN model checker (the executable should suffice). Make sure that you follow the installation instructions in every detail, since MOPED is rather hard to install. It is necessary to add the moped executable to your PATH after you have installed MOPED! Since the output of MOPED might have changed since BOOP was released, it is probably necessary to adjust the script that comes with BOOP.

Installing GCC 3.2 and the BOOP Toolkit v0.42
The installation of the BOOP Toolkit v0.42 and the GCC 3.2 compiler is described on a separate page!

Created by Georg Weißenbacher