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 12 articles , 2 standard articles )
Showing results 1 to 12 of 12.
- Jiang, Jiahong; Chen, Liqian; Wu, Xueguang; Wang, Ji: Block-wise abstract interpretation by combining abstract domains with SMT (2017)
- Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
- Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
- 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) ioport
- Albarghouthi, Aws; Gurfinkel, Arie; Li, Yi; Chaki, Sagar; Chechik, Marsha: UFO: verification with interpolants and abstract interpretation. (Competition contribution) (2013)
- 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)
- Piterman, Nir (ed.); Smolka, Scott A. (ed.): Tools and algorithms for the construction and analysis of systems. 19th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings (2013)
- Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: From under-approximations to over-approximations and back (2012)
- Albarghouthi, Aws; Li, Yi; Gurfinkel, Arie; Chechik, Marsha: Ufo: a framework for abstraction- and interpolation-based software verification (2012) ioport