Welcome to the Software Analysis Tool LLBMC!

Overview

LLBMC (the low-level bounded model checker) is a static software analysis tool for finding bugs in C (and, to some extent, in C++) programs. It is mainly intended for checking low-level system code and is based on the technique of Bounded Model Checking.

LLBMC logo
LLBMC can help to
  • reduce the time and effort needed for software testing,
  • improve the quality of software,
  • achieve high test coverage ratios,
  • obtain stable and secure software in reduced time.

LLBMC is fully automatic and requires minimal preparation efforts and user interaction. It supports all C constructs, including not so common features such as bitfields. LLBMC models memory accesses (heap, stack, global variables) with high precision and is thus able to find hard-to-detect memory access errors like heap or stack buffer overflows. LLBMC can also uncover errors due to uninitalized variables or other sources of non-deterministic behavior. Due to its precise analysis, LLBMC produces almost no false alarms (false positives).

Technically, LLBMC incorporates several innovations:

  • Instead of working on the C source code directly, it employs a compiler frontend (the LLVM compiler infrastructure) and starts verification on the RISC-assembler-like intermediate representation. LLBMC's analysis results are thus much closer to what actually runs on the machine.
  • LLBMC supports all C language features (currently with the exception of floating-point numbers), even esoteric ones like bitfields, and models their semantics with high precision on the bit-level.
  • By using an SMT solver (Boolector or STP) as a logical backend, it achieves high performance.
  • Rewrite-based simplifications can discharge many "easy" proof obligations before invocation of the core SMT solver. This again improves performance.

Built-in Checks

  • Integer overflow
  • Division by zero
  • Invalid bit shift
  • Illegal memory access (array index out of bound, illegal pointer access, etc.)
  • Invalid free
  • Double free
  • User-customizable checks (via __llbmc_assume / __llbmc_assert)