Solving Horn Clauses on Inductive Data Types Without Induction
This page contains supplementary material for the following paper
- E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Solving Horn Clauses on Inductive Data Types Without Induction.
Accepted to ICLP 2018, the
34th International Conference on Logic Programming
July 14-17 2018, Oxford, UK.
Benchmark suite and experiments
Our benchmark suite consists of 105 verification problems, each consisting of
an OCaml functional program manipulating inductively defined data structures
(such as lists or trees) together with a property to be verified.
We divide our benchmark suite into four sets of problems:
(1) FirstOrder, the set of problems relative to first-order programs (57 out of 70)
in the RCaml suite,
(2) HigherOrderInstances, the set of problems relative to first-order programs (13 out of 70)
that have been obtained by instantiating higher-order programs in the RCaml suite,
(3) MoreLists, a set of 16 verification problems on lists, and
(4) MoreTrees, a set of 19 verification problems on trees.
Download the benchmark suite
and the file containing detailed information about the experiments.
VeriMAP (for inductively
defined
data
types)
Download the VeriMAP-iddt tool.
Quick start
-----------
Get VeriMAP-idd from https://fmlab.unich.it/iclp2018/VeriMAP-iddt-linux_x86_64.tar.gz
$ wget https://fmlab.unich.it/iclp2018/VeriMAP-iddt-linux_x86_64.tar.gz
and run the following command
$ tar -zxvf VeriMAP-iddt-linux_x86_64.tar.gz
See the included README file for the instructions to run
VeriMAP-iddt on Debian/Ubuntu-based Linux distributions.
The package also includes the benchmark suite linked above.