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