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.

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 and ISP 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

For ParTypes, we have a detailed instruction presented in:
parTypesInstallation.txt