Repositories

The Vienna Verification Toolkit is comprised of the following components:

smtlib2 provides an common interface to various SMT solvers.
bindings-llvm is a low-level binding to the LLVM API for Haskell.
vvt contains all the programs of the Vienna Verification Toolkit.

Building

As a prequisite, you need to have a recent (version 7.8 or higher) GHC compiler and the cabal-install tool installed. The easiest way to grab both of them is to download and install the Haskell Platform. You further need to install version 3.5 of the LLVM framework and the clang compiler.

The first step is to build the SMTLib interface:

git clone https://github.com/hguenther/smtlib2.git
cd smtlib2
cabal install
cd backends/timing
cabal install
cd backends/debug
cabal install
cd extras/emulated-modulus
cabal install
cd ../..

The next step is to install the LLVM bindings. Usually this is just a simple

git clone https://github.com/hguenther/bindings-llvm.git
cd bindings-llvm
cabal install

However, if your LLVM installation is at an unusual place or you have different versions installed, it might be necessary to adjust the path to the llvm-config binary:

runghc Setup.hs configure --with-llvm-config=PATH
runghc Setup.hs build
runghc Setup.hs install

Lastly, we install the toolkit:

git clone https://github.com/hguenther/vvt.git
cd vvt
cabal install