PE is a tool for partially evaluating Constrained Horn clauses.
PE is written in Ciao and is interfaced with Parma Polyhedra library and Yices SMT solver for handling constraints.
Ciao 1.16 or newer (installed
from git repository with ./ciao-boot.sh local-install)
The following dependendencies (including third-party code) need to 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) - CHCLibs (
ciao get github.com/bishoksan/chclibs)
Note: Installing RAHFT (ciao get github.com/bishoksan/RAHFT) includes installation of all the above dependencies, and the Yices and PPL libraries.
- dot for drawing control flow graphs.
PE is carried out with respect to a fixed set of properties. Properties are generated using the props.pl or props1.pl programs
- See shell script pe.sh
PE is used as the central component in a control-flow refinement algorithm.
- See shell script cfr.sh
PE is used in an iterative algorithm for checking safety of a set of CHCs.
- See shell script safe.sh
(Does not use PE). Strengthens constraints in a set of CHCs with respect to an entry goal, adding invariants to the clause bodies.
- See shell script spec.sh