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)