Refinement of Abstraction in Horn clauses using Finite Tree automata (RAHFT)
RAHFT is a tool based on abstraction refinement for verifying
Constrained Horn clauses using abstract interpretation and finite tree
automata. The correctness of results are with respect to the
input Horn clauses and over the theory
linear integer arithmetic.
RAHFT is written in Ciao and is interfaced with Parma polyhedra library and Yices SMT solver for handling constraints. RAHFT uses several reusable components such as Convex polyhedra analyser, Query-answer tranformer etc. It also includes a Java library for manipulating finite tree automata.
Ciao 1.16 or newer (installed
from git repository with
Build and installation
You can automatically fetch, build, and install RAHFT using:
ciao get github.com/bishoksan/RAHFT
The following dependendencies (including third-party code) will be installed automatically:
- Ciao bindings for
Parma Polyhedra Library
ciao get ciao_ppl)
- Ciao bindings for
Yices SMT solver
ciao get github.com/jfmc/ciao_yices)
ciao get github.com/bishoksan/chclibs)
All code will be downloaded and built under the first directory
specified in the
CIAOPATH environment variable or
For developing it is recommended to define your own
workspace directory and clone this repository. E.g.,
export CIAOPATH=~/ciao and update your
The dependencies can be cloned manually or fetched automatically by
ciao fetch at the source directory.
rahft <input file containing a set of Horn clauses>
Input: a set of Horn clauses together with integrity constraints. They are written using Prolog notation:
e.g. a clause is written as:
h(X):- C, b1(X1),...,bn(Xn).
and an integrity constriant is written as
false :- C, b1(X1),...,bn(Xn).
The results of the analysis will be appended to the
result.txt file in the current directory and also shown in the console.
Generate a standalone binary distribution
mkdir dist; cd dist ciaoc_sdyn ../src/rahft cp ../src/determinise.jar
This creates a platform specific binary
directory, together with the collection of shared libraries for the
Horn clause verification with convex polyhedral abstraction and tree automata-based refinement by Bishoksan Kafle and John P. Gallagher in COMLAN 2015 (http://www.sciencedirect.com/science/article/pii/S1477842415000822).
Tree Automata-Based Refinement with Application to Horn Clause Verification by Bishoksan Kafle and John P. Gallagher in VMCAI 2015 (http://link.springer.com/chapter/10.1007%2F978-3-662-46081-8_12#page-1)
Constraint Specialisation in Horn Clause Verification by Bishoksan Kafle and John P. Gallagher in PEPM 2015 (http://akira.ruc.dk/~kafle/publications/pepm-15)
Rahft: A tool for verifying Horn clauses using abstract interpretation and finite tree automata by Bishoksan Kafle, John P. Gallagher and Jose F. Morales to appear in CAV 2016.