This is the whole experiments suite used for the VMCAI 17 paper.

We categories our experiments suites as follows:
CIVLTests/: examples from CIVL regression tests.
ISPTests/:  examples from ISP' example website [http://formalverification.cs.utah.edu/ISP_Tests/].
TASSTests/: examples from TASS example suites.
GecoTests/: public examples downloaded from [http://geco.mines.edu/prototype/Show_me_some_local_HPC_tutorials/examples/mpi/]
FeatureTests/: a set of examples which illustrate features provided by different tools.

We provide benchmarks of ParTypes and MOPPER as well in:
ParTypes/
bc-for-Mopper/

Artifacts used in our scalability tests are in:
Scalability/


Tools we used:
CIVL v1.7.2: [http://vsl.cis.udel.edu/lib/sw/civl/1.7.2/latest/]
ISP  v0.3.1: [http://www.cs.utah.edu/formal_verification/ISP-release/tarball/isp-0.3.1.tar.gz]
MOPPER: [https://github.com/subodhvsharma/mopper-spo.git]
MPI-Spin: v1.0: [http://vsl.cis.udel.edu/mpi-spin/index.html]
ParTypes: v1.0.3: [http://gloss.di.fc.ul.pt/ParTypes/downloads]


INSTALL: We have no problem for installing CIVL, MPI-Spin, ISP and
ParTypes on the platform we mentioned in the paper by following the
provided instructions. For MOPPER, we provides our installation
instructions here, in case people encounter same problems we had
during installation:

1) Install the solver
   Go to the lingeling directory and type make
   Go to the solver directory
   make

2) Install necessary softwares: autoconf, libopts
   sudo apt-get install autoconf
   sudo apt-get install libopts25

3) do "autoreconf"

4) Install ISP+MOPPER 
   ./configure --prefix="Some Directory" --disable-gui --enable-optional-ample-set-fix --with-mpi-inc-dir=<path to mpi.h file>
   make
   make install
