The bounded model checker LLBMC

Stephan Falke, Florian Merz, Carsten Sinz

DOI 10.1109/ase.2013.6693138 dblp

Abstract

This paper presents LLBMC, a tool for finding bugs and runtime errors in sequential C/C++ programs. LLBMC employs bounded model checking using an SMT-solver for the theory of bitvectors and arrays and thus achieves precision down to the level of single bits. The two main features of LLBMC that distinguish it from other bounded model checking tools for C/C++ are (i) its bit-precise memory model, which makes it possible to support arbitrary type conversions via stores and loads; and (ii) that it operates on a compiler intermediate representation and not directly on the source code.

BibTeX

@inproceedings{Falke-al:ASE13,
  author    = {Stephan Falke and
               Florian Merz and
               Carsten Sinz},
  title     = {The bounded model checker {LLBMC}},
  booktitle = {ASE},
  pages     = {706--709},
  publisher = {{IEEE}},
  year      = {2013},
}

The bounded model checker LLBMC

Abstract

Related papers