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
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
- Kiefer, Moritz; Klebanov, Vladimir; Ulbrich, Mattias: Relational program reasoning using compiler IR (2018)
- 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)
- Fedyukovich, Grigory; Sharygina, Natasha: Towards completeness in bounded model checking through automatic recursion depth detection (2015)
- Iser, Markus; Manthey, Norbert; Sinz, Carsten: Recognition of nested gates in CNF formulas (2015)
- Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013) ioport
- Falke, Stephan; Merz, Florian; Sinz, Carsten: LLBMC: improved bounded model checking of C programs using LLVM . (Competition contribution) (2013) ioport
- 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)
- 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)
- Merz, Florian; Falke, Stephan; Sinz, Carsten: LLBMC: bounded model checking of C and C++ programs using a compiler IR (2012) ioport
- Sinz, Carsten; Merz, Florian; Falke, Stephan: LLBMC: a bounded model checker for LLVM’s intermediate representation (competition contribution) (2012) ioport