×

LLBMC

swMATH ID: 9478
Software Authors: Falke, Stephan; Merz, Florian; Sinz, Carsten
Description: 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.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-642-36742-7_48
Related Software: CBMC; UFO; CPAchecker; MiniSat; z3; BLAST; Lingeling; Plingeling; Yices; SLAM; Smallfoot; SLAyer; Predator; SMACK; SeaHorn; AProVE; LLVM; ESBMC; JPF-SE; DynAlloy
Referenced in: 12 Publications

Standard Articles

1 Publication describing the Software Year
LLBMC: improved bounded model checking of C programs using LLVM . (Competition contribution)
Falke, Stephan; Merz, Florian; Sinz, Carsten
2013

Referencing Publications by Year