SATABS Manual

Installing SATABS

Requirements

SATABS is available for Windows, i86 Linux, and MacOS X. SATABS requires a code pre-processing environment comprising of a suitable preprocessor and an a set of header files.

1. Linux: the preprocessor and the header files typically come with a package called gcc, which must be installed prior to the installation of SATABS.
2. Windows: The Windows version of SATABS requires the preprocessor cl.exe, which is part of Visual Studio (including the free Visual Studio Express).
3. MacOS: Install XCode prior to installing SATABS.

Important note for Windows users: Visual Studio's cl.exe relies on a complex set of environment variables to identify the target architecture and the directories that contain the header files. You must run SATABS from within the Visual Studio Command Prompt.

Note that the distribution files for the Eclipse plugin include the command-line tools. Therefore, if you intend to run SATABS exclusively within Eclipse, you can skip the installation of the command-line tools. However, you still have to install the compiler environment as described above.

Choosing and Installing a Model Checker

You need to install a Model Checker in order to be able to run SATABS. You can choose between following alternatives:

• Cadence SMV. Available from http://www.kenmcmil.com/smv.html. Cadence SMV is a commercial model checker. The free version that is available on the homepage above must not be used for commercial purposes (read the license agreement thoroughly before you download the tool). The documentation for SMV can be found in the directory where you unzip/untar SMV under ./smv/doc/smv/. Read the installation instructions carefully. The Linux/MacOS versions require setting environment variables. You must add add the directory containing the smv binary (located in ./smv/bin/, relative to the path where you unpacked it) to your PATH environment variable. SATABS uses Cadence SMV by default.

• NuSMV. Available from http://nusmv.irst.itc.it/. NuSMV is the open source alternative to Cadence SMV. Installation instructions and documentation can be found on the NuSMV homepage. The directory containing the NuSMV binary should be added to your PATH environment variable. Use the option

  --modelchecker nusmv

  to instruct SATABS to use NuSMV.

• BOPPO. Available from http://www.cprover.org/boppo/. BOPPO is a model checker that uses SAT-solving algorithms. BOPPO relies on a built-in SAT solver and Quantor, a solver for quantified boolean formulas that is currently bundled with BOPPO, but also available separately from http://fmv.jku.at/quantor/. We recommend to add the directories containing both tools to your PATH environment variable. Use the option

  --modelchecker boppo

  when you call SATABS and want it to use BOPPO instead of SMV.

• BOOM. Available from http://www.cprover.org/boom/. Boom has a number of unique features, including the verification of programs with unbounded thread creation.

Installing SATABS

1. Download SATABS for your operating system. The binaries are available from http://www.cprover.org/satabs/.
2. Unzip/untar the archive into a directory of your choice. We recommend to add this directory to your PATH environment variable.

Now you can execute SATABS. Try running SATABS on the small examples presented in the tutorial section. If you use the Cadence SMV model checker, the only command line arguments you have to specify are the names of the files that contain your program.