LLBMC: The Low-Level Bounded Model Checker

Google Tech Talk (more info below) February 22, 2011 Presented by Carsten Sinz, Stephan Falke, & Florian Merz, Karlsruhe Institute of Technology, Germany. ABSTRACT Producing reliable and secure software is time consuming and cost intensive, and still many software systems suffer from security vulnerabilities or show unintended, faulty behavior. Testing is currently the predominant method to ascertain software quality, but over the last years formal methods like abstract interpretation or model checking made huge progress and became applicable to real-world software systems. Their promise is to reach a much higher level of software quality with less effort. In this talk we present a recent method for systematic bug finding in C programs called Bounded Model Checking (BMC) that works fully automatic and achieves a high level of precision. We present our implementation, LLBMC, which---in contrast to other tools---doesn't work on the source code level, but employs a compiler intermediate representation (LLVM IR) as a starting point. It is thus easily adaptable to support verification of other programming languages such as C++ or ObjC. LLBMC also uses a highly precise (untyped) memory model, which allows to reason about heap and stack data accesses. Moreover, we show how LLBMC can be integrated into the software development process using a technique called Abstract Testing.