Wiki
Clone wikiufo / svcomp13
This page is the submission of the UFO software verifier to the 2013 Competition on Software Verification (SV-COMP).
Team
Arie Gurfinkel, Aws Albarghouthi, Yi Li, Sagar Chaki, and Marsha Chechik
Tool
Download: https://bitbucket.org/arieg/ufo/downloads/ufo-svcomp13.tar.gz
Requirements
- Multiprecision arithmetic library (C++ bindings).
sudo apt-get install libgmpxx4ldbl
Installation
- Untar:
tar xvzf ufo-svcomp13.tar.gz
Run
PATH_TO_UFO/bin/ufo-svcomp-par.py [OPTIONS] file
Options
-m64
sets int to 32 bits and long and pointer types to 64 bits--ufo-track--ptr
tracks pointers in addition to numeric variables--cex=FILE
enables counter-example generation to FILE
Categories
- UFO is participating in ControlFlowIntegers, ProductLines, DeviceDrivers64, SystemC, Loops, and FeatureChecks
- All categories except for DeviceDrivers64 do not require any options
- DeviceDrivers64 requires
-m64 --ufo-track-ptr
Results
Output contains the string Result SAFE
when the program is safe and the string Result CEX
when a counterexample is found.
Preliminary results from the training phase are available at: http://arieg.bitbucket.org/ufo/svcomp13/
Contact
For additional information please contact Arie Gurfinkel (arie at cmu dot edu) or Aws Albarghouthi (aws at cs dot toronto dot edu)
Updated