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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element


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

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

  1. 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)
  2. Fedyukovich, Grigory; Sharygina, Natasha: Towards completeness in bounded model checking through automatic recursion depth detection (2015)
  3. Iser, Markus; Manthey, Norbert; Sinz, Carsten: Recognition of nested gates in CNF formulas (2015)
  4. Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013)
  5. Falke, Stephan; Merz, Florian; Sinz, Carsten: LLBMC: improved bounded model checking of C programs using LLVM . (Competition contribution) (2013)
  6. 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)
  7. 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)
  8. Merz, Florian; Falke, Stephan; Sinz, Carsten: LLBMC: bounded model checking of C and C++ programs using a compiler IR (2012) ioport
  9. Sinz, Carsten; Merz, Florian; Falke, Stephan: LLBMC: a bounded model checker for LLVM’s intermediate representation (competition contribution) (2012) ioport