VeriMAP is capable of: (i) generating the CHC encoding of a verification problem, and (ii) improving the effectiveness and the efficiency of CHC solvers by applying transformations of CHCs.
The tool is, to a large extent, parametric with respect to the languages in which the program and the property to be verified are written, and allows the user to take advantage of the very effective techniques and tools that have been developed in the fields of constraint logic programming and SMT solving.