Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. 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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Fedyukovich, Grigory; Gurfinkel, Arie; Sharygina, Natasha: Automated discovery of simulation between programs (2015)
- Khoroshilov, Alexey; Mutilin, Vadim; Novikov, Evgeny; Zakharov, Ilja: Modeling environment for static verification of Linux kernel modules (2015)
- Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015)
- Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013)
- Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto: The mathsat5 SMT solver (2013)
- Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: From under-approximations to over-approximations and back (2012)