VeriCaT

Instructions for installing and running VeriCaT, a tool implementing a catamorphism-based transformation algorithm. These instructions have been tested on Ubuntu 20.04 LTS.

Extract the VeriCaT-linux_x86_64.tar.gz archive and change directory by typing

tar xzf VeriCaT-linux_x86_64.tar.gz
cd VeriCaT-linux_x86_64
Install SWI-Prolog and its dependencies

sudo dpkg -i packages/*.deb
Run VeriCaT

./VeriCaT <spec> [<property>]
where
- <spec> is the name of a file containing a CHC specification in Prolog format
- <property> is the predicate defining the negation of the contract to be checked (optional, default value: ff1)

Note that the names of the files in the Benchmarks/ directory are of the form <example>-<d>.pl where <example> is a string describing the program and <d> is an integer denoting that the specification file includes <d> properties named ff1,...,ff<d>.

For instance, the specification file Benchmarks/REV-sort-01-isASorted_rev_isDSorted-leq_all--iff-2.pl contains two properties, ff1 and ff2, that can be checked by running VeriCaT as follows:

./VeriCaT Benchmarks/REV-sort-01-isASorted_rev_isDSorted-leq_all--iff-2.pl ff1
./VeriCaT Benchmarks/REV-sort-01-isASorted_rev_isDSorted-leq_all--iff-2.pl ff2