LLBMC

LLBMC: improved bounded model checking of C programs using LLVM . (Competition contribution). LLBMC is a tool for detecting bugs and runtime errors in C and C++ programs. It is based on bounded model checking using an SMT solver and thus achieves bit-accurate precision. A distinguishing feature of LLBMC in contrast to other bounded model checking tools for C programs is that it operates on a compiler intermediate representation and not directly on the source code.


References in zbMATH (referenced in 15 articles , 1 standard article )

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

  1. Lu, Xu; Duan, Zhenhua; Tian, Cong; Du, Hongwei: Verify heaps via unified model checking (2020)
  2. Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems (2020)
  3. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  4. Duck, Gregory J.; Jaffar, Joxan; Yap, Roland H. C.: Shape neutral analysis of graph-based data-structures (2018)
  5. Kiefer, Moritz; Klebanov, Vladimir; Ulbrich, Mattias: Relational program reasoning using compiler IR (2018)
  6. 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)
  7. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view (2016)
  8. Fedyukovich, Grigory; Sharygina, Natasha: Towards completeness in bounded model checking through automatic recursion depth detection (2015)
  9. Iser, Markus; Manthey, Norbert; Sinz, Carsten: Recognition of nested gates in CNF formulas (2015)
  10. Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013) ioport
  11. Falke, Stephan; Merz, Florian; Sinz, Carsten: LLBMC: improved bounded model checking of C programs using LLVM . (Competition contribution) (2013) ioport
  12. 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)
  13. Flanagan, Cormac (ed.); König, Barbara (ed.): Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012. Proceedings (2012)
  14. Merz, Florian; Falke, Stephan; Sinz, Carsten: LLBMC: bounded model checking of C and C++ programs using a compiler IR (2012) ioport
  15. Sinz, Carsten; Merz, Florian; Falke, Stephan: LLBMC: a bounded model checker for LLVM’s intermediate representation (competition contribution) (2012) ioport