UFO: A Framework for Abstraction- and Interpolation-Based Software Verification

Aws Albarghouthi, Yi Li, Arie Gurfinkel, and Marsha Chechik

In Proceedings of the 24th International Conference on Computer Aided Verification (CAV), 2012

Abstract: In this paper, we present UFO, 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. We have built three instantiations of the framework: a predicate abstraction-based version, an interpolationbased version, and a combined version which uses a novel and powerful combination of interpolation-based and predicate abstraction-based algorithms.

Cite:

@inproceedings{Albarghouthi2012UFO,
  author = {Albarghouthi, Aws and Li, Yi and Gurfinkel, Arie and Chechik, Marsha},
  booktitle = {Proceedings of the 24th International Conference on Computer Aided Verification (CAV)},
  month = jul,
  pages = {672--678},
  title = {{UFO}: A Framework for Abstraction- and Interpolation-Based Software Verification},
  year = {2012}
}