Relational Properties Verification through Horn Clause Transformation

This page contains supplementary material for the following paper

• E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti. Relational Verification through Horn Clause Transformation. Proceedings of the 23rd Static Analysis Symposium (SAS 2016). Lecture Notes in Computer Science (LNCS), vol. 9837, Springer, 2016, pp. 147-169.

• E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti. Verifying Relational Program Properties by Transforming Constrained Horn Clauses. Proceedings of the 31st Italian Conference on Computational Logic (CILC 2016). CEUR Workshop Proceedings vol. 1645, CEUR-WS.org, 2016, pp.69-85.

VeriMAPrel

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

• VeriMAPrel, 64-bit Linux binary
• XUbuntu 14.04 VM + VeriMAPrel (about 1.5GB). Password: 'sas2016' without quotes.
• Benchmark set (C programs)

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).