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 interpolation-based version, and a combined version which uses a novel and powerful combination of interpolation-based and predicate abstraction-based algorithms. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Albarghouthi, A., Li, Y., Gurfinkel, A., & Chechik, M. (2012). Ufo: A framework for abstraction- and interpolation-based software verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7358 LNCS, pp. 672–678). https://doi.org/10.1007/978-3-642-31424-7_48
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
