We present VeriMAP, a tool for the verification of C programs based on the transformation of constraint logic programs, also called constrained Horn clauses. VeriMAP makes use of Constraint Logic Programming (CLP) as a metalanguage for representing: (i) the operational semantics of the C language, (ii) the program, and (iii) the property to be verified. Satisfiability preserving transformations of the CLP representations are then applied for generating verification conditions and checking their satisfiability. VeriMAP has an interface with various solvers for reasoning about constraints that express the properties of the data (in particular, integers and arrays). Experimental results show that VeriMAP is competitive with respect to state-of-the-art tools for program verification.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M. (2014). VeriMAP: A tool for Verifying Programs through Transformation.. In Tools and Algorithms for the Construction and Analysis of Systems (pp.568-574). BERLIN -- DEU : Springer Berlin Heidelberg.
VeriMAP: A tool for Verifying Programs through Transformation.
PETTOROSSI, ALBERTO;
2014-01-01
Abstract
We present VeriMAP, a tool for the verification of C programs based on the transformation of constraint logic programs, also called constrained Horn clauses. VeriMAP makes use of Constraint Logic Programming (CLP) as a metalanguage for representing: (i) the operational semantics of the C language, (ii) the program, and (iii) the property to be verified. Satisfiability preserving transformations of the CLP representations are then applied for generating verification conditions and checking their satisfiability. VeriMAP has an interface with various solvers for reasoning about constraints that express the properties of the data (in particular, integers and arrays). Experimental results show that VeriMAP is competitive with respect to state-of-the-art tools for program verification.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.