Web interface for remote use of VeriMAP (click here)


Emanuele De Angelis, Fabio Fioravanti, and Maurizio Proietti


De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: A Tool for Verifying Programs through Transformations. Tool demonstration paper. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). ETAPS '14, Grenoble, France, 2014.

October 12, 2013

VeriMAP is a tool for the verification of C programs based 
on the transformation of constraint logic programs.

Quick start
Download VeriMAP from 
and run the following commands: 

  tar -zxvf VeriMAP-linux_x86_64.tar.gz
  cd VeriMAP-linux_x86_64


Getting basic help


Getting advanced help

./VeriMAP --help 

Verifying a program (for instance, example1.c) with basic options

./VeriMAP examples/example1.c

Generating the CLP program from the C program

./VeriMAP examples/example1.c --c2clp

Generating the Verification Conditions (VC's)

./VeriMAP examples/example1.c --vcg

Setting a number of iterations for the Iterated Verifier

./VeriMAP examples/example1.c --iterations N

Changing strategy: to choose a strategy to deal with programs that manipulate 
(i) integers ('w' or 'ch-w'), and (ii) integers and arrays ('array').

./VeriMAP examples/example1.c --strategy {w,ch-w,array}

('w' stands for 'widening', 'ch-w' stands for 'convex hull and widening')


To run the paper examples:

./VeriMAP examples/example1.c
./VeriMAP examples/example2.c --iterations 2

To run an example (for instance, integer.c) in the 'integers' folder
by executing at most N iterations(*):

./VeriMAP examples/integers/integer.c --strategy ch-w --iterations N

(*) we recommend you to use 8 as a value for N.

To run an example (for instance, array.c) in the 'arrays' folder:

./VeriMAP examples/arrays/array.c --strategy array