VeriMAP

Download

Web interface for remote use of VeriMAP (click here)

Developers

Emanuele De Angelis, Fabio Fioravanti, and Maurizio Proietti

Paper

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.

 
README for VeriMAP
------------------
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 http://map.uniroma2.it/VeriMAP/ 
and run the following commands: 

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

Usage
-----

Getting basic help

./VeriMAP


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


Examples
--------

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