×

UFO

swMATH ID: 9570
Software Authors: Aws Albarghouthi, Yi Li, Arie Gurfinkel, Marsha Chechik
Description: 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.
Homepage: http://link.springer.com/chapter/10.1007/978-3-642-31424-7_48
Related Software: CPAchecker; z3; BLAST; SLAM; SatAbs; CBMC; KLEE; SMTInterpol; LLVM; LLBMC; SMACK; Wolverine; Threader; GitHub; Cascade; VCC; Spacer; Houdini; SeaHorn; Predator
Cited in: 18 Publications

Standard Articles

2 Publications describing the Software, including 1 Publication in zbMATH Year
UFO: verification with interpolants and abstract interpretation. (Competition contribution)
Albarghouthi, Aws; Gurfinkel, Arie; Li, Yi; Chaki, Sagar; Chechik, Marsha
2013
From under-approximations to over-approximations and back. Zbl 1352.68140
Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha
2012
all top 5

Cited by 65 Authors

3 Fedyukovich, Grigory
3 Gurfinkel, Arie
2 Podelski, Andreas
2 Sharygina, Natasha
1 Albarghouthi, Aws
1 Alt, Leonardo S.
1 Aschermann, Cornelius
1 Bansal, Kshitij
1 Baranowski, Marek
1 Barrett, Clark W.
1 Bernasconi, Anna
1 Beyer, Dirk
1 Bodik, Rastislav
1 Brockschmidt, Marc
1 Chaki, Sagar
1 Chechik, Marsha
1 Chen, Liqian
1 Cimatti, Alessandro
1 Cook, Byron
1 Dangl, Matthias
1 Dietsch, Daniel
1 Frohn, Florian
1 Fuhs, Carsten
1 Gange, Graeme
1 Garzella, Jack J.
1 Giesl, Jürgen
1 Greitschus, Marius
1 Griggio, Alberto
1 Hajdu, Ákos
1 He, Shaobo
1 Hensel, Jera
1 Hyvärinen, Antti E. J.
1 Jančík, Pavel
1 Jhala, Ranjit
1 Jiang, Jiahong
1 Kaufman, Samuel J.
1 Khazem, Kareem
1 King, Tim
1 Kofroň, Jan
1 Komuravelli, Anvesh
1 Kröning, Daniel
1 Menghi, Claudio
1 Micskei, Zoltán
1 Navas, Jorge A.
1 Piterman, Nir
1 Rakamarić, Zvonimir
1 Reynolds, Andrew
1 Rizzi, Alessandro Maria
1 Rybalchenko, Andrey
1 Schaafsma, Bastiaan Joost
1 Schachte, Peter
1 Schneider-Kamp, Peter
1 Sebastiani, Roberto
1 Smolka, Scott A.
1 Søndergaard, Harald
1 Spoletini, Paola
1 Ströder, Thomas
1 Stuckey, Peter James
1 Tasiran, Serdar
1 Tautschnig, Michael
1 Tuttle, Mark R.
1 Wang, Ji
1 Wendler, Philipp
1 Wies, Thomas
1 Wu, Xueguang

Cited in 5 Serials

4 Formal Methods in System Design
3 Journal of Automated Reasoning
1 Formal Aspects of Computing
1 Theory and Practice of Logic Programming
1 Lecture Notes in Computer Science

Cited in 3 Fields

18 Computer science (68-XX)
3 Mathematical logic and foundations (03-XX)
1 General and overarching topics; collections (00-XX)

Citations by Year