Semantics-based generation of verification conditions by program specialization

• Benchmark set (C programs)
• VCs SS1 (qarmc, msatic3, z3)
• VCs MS1 (qarmc, msatic3, z3)

Tool

• VeriMAP-linux_x86_64.tar.gz

 
README for VeriMAP-vcg
----------------------
July 06, 2015

VeriMAP-vcg is a tool for generating the Verification Conditions (VCs) 
of C programs based on the transformation of constraint logic programs.


Quick start
-----------
Download VeriMAP from http://map.uniroma2.it/vcgen/ 
and run the following commands: 

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

Usage
-----

Getting help

./VeriMAP --help 

Generating the VCs by using the interpreter for the small-step semantics

./VeriMAP-vcg example.c configs/vcg_SS1.iteration

Generating the VCs by using the interpreter for the multi-step semantics

./VeriMAP-vcg example.c configs/vcg_MS1.iteration

Generating the VCs and converting them to the specified format 

./VeriMAP-vcg example.c configs/vcg_SS1.iteration --convert-to $FORMAT

where $FORMAT is either 'smt-msatic3' for the msatic3 solver, 
or 'smt-z3' for the Z3 SMT solver, or 'horn-eldarica' for the eldarica solver.

The generated VCs, and its translation (whenever the --convert-to option applies),
can be found in OutProgs-vcg