UFO is a framework (and a tool) for verifying (and finding bugs in) sequential C programs. The framework is built on top of the LLVM compiler infrastructure and is targeted at researchers designing and experimenting with verification algorithms. It allows definition of different abstract post operators, refinement strategies and exploration strategies. Currently, there are several instantiations of the framework including a predicate abstraction-based version, an interpolation-based version, and a combined version which uses a novel and powerful combination of interpolation-based and predicate abstraction-based algorithms, and an abstract-interpretation based version.

Documentation | Publications | FAQ | ReleaseNotes

News

• June 11, 2014: Simplified compilation process for Symba. https://bitbucket.org/arieg/symba
• February 12, 2014: SV-COMP'14 results and binaries
• September 12, 2013: symbolic optimization tool -- Symba (POPL'14 version) released as a part of UFO. Obtain a linux binary from here. See README.md for additional documentation.
• March 16, 2013: UFO front-end released: http://bitbucket.org/arieg/ufofe.
• December 15, 2012: UFO wins ControlFlowInteger, DeviceDrivers64, ProductLines, and SystemC categories of SV-COMP'13 (binaries)
• First version released

Older News

Supported Platforms

• Linux/Ubuntu
• OS X

Documentation

• Online Documentation

Mailing Lists

For any questions or comments on UFO, please post to UFO's mailing lists:

• UFO discussion list: for general questions and discussion
• UFO developers list: for development of UFO
• UFO commits list: for commit messages