Theory and Implementation of Software Bounded Model Checking

This thesis provides a detailed overview of the theory of software bounded model checking (SBMC) and its implementation in LLBMC, which is based on the LLVM compiler framework. The whole process from a C program to an SMT formula is described in detail. Furthermore, a theory of dynamic memory allocation is introduced which allows modelling C's memory model with high precision. Finally, it is shown that LLBMC's approach to software bounded model checking performs well compared to competing tools.