UFO

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.


References in zbMATH (referenced in 23 articles , 2 standard articles )

Showing results 1 to 20 of 23.
Sorted by year (citations)

1 2 next

  1. Cook, Byron; Khazem, Kareem; Kroening, Daniel; Tasiran, Serdar; Tautschnig, Michael; Tuttle, Mark R.: Model checking boot code from AWS data centers (2021)
  2. Menghi, Claudio; Rizzi, Alessandro Maria; Bernasconi, Anna; Spoletini, Paola: TOrPEDO : witnessing model correctness with topological proofs (2021)
  3. Fedyukovich, Grigory; Kaufman, Samuel J.; Bodík, Rastislav: Learning inductive invariants by sampling from frequency distributions (2020)
  4. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  5. Hajdu, Ákos; Micskei, Zoltán: Efficient strategies for CEGAR-based model checking (2020)
  6. Jančík, Pavel; Kofroň, Jan; Alt, Leonardo; Fedyukovich, Grigory; Hyvärinen, Antti E. J.; Sharygina, Natasha: Exploiting partial variable assignment in interpolation-based model checking (2019)
  7. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  8. Jhala, Ranjit; Podelski, Andreas; Rybalchenko, Andrey: Predicate abstraction for program verification (2018)
  9. Greitschus, Marius; Dietsch, Daniel; Podelski, Andreas: Loop invariants from counterexamples (2017)
  10. Jiang, Jiahong; Chen, Liqian; Wu, Xueguang; Wang, Ji: Block-wise abstract interpretation by combining abstract domains with SMT (2017)
  11. 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)
  12. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  13. Bansal, Kshitij; Reynolds, Andrew; King, Tim; Barrett, Clark; Wies, Thomas: Deciding local theory extensions via E-matching (2015)
  14. Fedyukovich, Grigory; Gurfinkel, Arie; Sharygina, Natasha: Automated discovery of simulation between programs (2015)
  15. Gange, Graeme; Navas, Jorge A.; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: Horn clauses as an intermediate representation for program analysis and transformation (2015)
  16. Khoroshilov, Alexey; Mutilin, Vadim; Novikov, Evgeny; Zakharov, Ilja: Modeling environment for static verification of Linux kernel modules (2015) ioport
  17. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  18. Albarghouthi, Aws; Gurfinkel, Arie; Li, Yi; Chaki, Sagar; Chechik, Marsha: UFO: verification with interpolants and abstract interpretation. (Competition contribution) (2013) ioport
  19. Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013) ioport
  20. Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto: The MathSAT5 SMT solver (2013)

1 2 next