Building PathFinder

The following contains instructions to get a working PathFinder build. PathFinder only runs on Linux.

Downloading PathFinder

You can get the sources over at Github, or use this direct link to the ZIP archive.

Requirements

bam

PathFinder uses the bam build system. Get it from Github or install the Debian package:

    apt-get install bam

OTAWA

Get it at http://otawa.fr/. You will need OTAWA v2. If you run into trouble with dependencies on Debian, I suggest using

    apt-get install flex bison bzr g++ ocaml libxml2-dev libxslt-dev mercurial

An SMT solver

PathFinder supports two SMT solvers, CVC4 and z3. You can use either with very comparable performances and almost identical outputs.

CVC4

If you have admin rights on your machine, you can get CVC4 with an automated script:

    ./get_cvc4.sh

You may also want to try a local install (which can be trickier) with

    ./get_cvc4_local/all.sh

Z3

Z3 tends to be significantly less tricky to install. You can follow the instructions at https://github.com/Z3Prover/z3.

Installing PathFinder

To install, type bam and follow the instructions. bam config will run a default config, which you can reset by removing the config.lua file. In order to select either solver, use bam config solver=cvc4 or bam config solver=z3.

Alternatively, you can use ./make_cvc4 or ./make_z3.

Note: In order to run PathFinder with maximum performance (for benchmarking), you must run bam config O=3 debug=false warnings=false v1=false.

Note: If your terminal does not support UTF-8, use bam config utf8=false