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

Disclaimer 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: HOL98 Theorem Prover PROSPER Toolkit MOPED model checker GCC 3.2 sources 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) in 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 in {sec=sec, usec=0} end 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) end 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 bopCallMoped.pl 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