Relational Properties Verification through Horn Clause Transformation

This page contains supplementary material for the following paper

a preliminary version of which was published as


The VeriMAPrel tool for verifying relational properties is available for download both as a pre-compiled binary and as a Virtualbox virtual machine.

VeriMAPrel is built upon VeriMAP, a tool for the verification of C programs based on the transformation of Constraint Logic Programs (also known as Constrained Horn Clauses).