Welcome to the Software Analysis Tool LLBMC!
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.
- 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 perparation 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.
- 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)