Publications

2013

  • Stephan Falke, Florian Merz, and Carsten Sinz:
    The Bounded Model Checker LLBMC (Tool Demonstration)
    In Proceedings of the 28th International Conference on Automated Software Engineering (ASE '13), Palo Alto, USA.
    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
  • Stephan Falke, Florian Merz, and Carsten Sinz:
    Extending the Theory of Arrays: memset, memcpy, and Beyond
    In Proceedings of the 5th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '13), Atherton, USA. ©Springer-Verlag
    The theory of arrays is widely used in program analysis, (deductive) software verification, bounded model checking, and symbolic execution to model arrays in programs or the computer's main memory. Nonetheless, the theory as introduced by McCarthy is not expressive enough in many practical cases since it only supports array updates at single locations. In programs, memory is often modified at multiple locations at once using functions such as memset or memcpy. Furthermore, initialization loops that store counter-dependent values in an array are commonly used. This paper presents an extension of the theory of arrays with λ-terms which makes it possible to reason about such cases. We also discuss how loops can be automatically summarized using such λ-terms.
  • Stephan Falke, Florian Merz, and Carsten Sinz:
    LLBMC: Improved Bounded Model Checking of C Programs Using LLVM (Competition Contribution)
    In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '13), Rome, Italy. ©Springer-Verlag
    LLBMC is a tool for detecting bugs and runtime errors in C and C++ programs. It is based on bounded model checking using an SMT solver and thus achieves bit-accurate precision. A distinguishing feature of LLBMC in contrast to other bounded model checking tools for C programs is that it operates on a compiler intermediate representation and not directly on the source code.

2012

  • Stephan Falke, Carsten Sinz, and Florian Merz:
    A Theory of Arrays with Set and Copy Operations (Extended Abstract)
    In Proceedings of the 10th International Workshop on Satisfiability Modulo Theories (SMT '12), Manchester, UK.
    The theory of arrays is widely used in order to model main memory in program analysis, software verification, bounded model checking, symbolic execution, etc. Nonetheless, the basic theory as introduced by McCarthy is not expressive enough for important practical cases, since it only supports array updates at single locations. In programs, memory is often modified using functions such as memset or memcpy/memmove, which modify a user-specified range of locations whose size might not be known statically. In this paper we present an extension of the theory of arrays with set and copy operations which make it possible to reason about such functions. We also discuss further applications of the theory.
  • Carsten Sinz, Florian Merz, and Stephan Falke:
    LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation (Competition Contribution)
    In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '12), Tallinn, Estonia. ©Springer-Verlag
    We present LLBMC, a bounded model checker for C programs. LLBMC uses the LLVM compiler framework in order to translate C programs into LLVM's intermediate representation (IR). The resulting code is then converted into a logical representation and simplified using rewrite rules. The simplified formula is finally passed to an SMT solver. In contrast to many other tools, LLBMC uses a flat, bit-precise memory model. It can thus precisely model, e.g., memory-based re-interpret casts.
  • Florian Merz, Stephan Falke, and Carsten Sinz:
    LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR
    In Proceedings of the 4th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '12), Philadelphia, USA. ©Springer-Verlag
    Bounded model checking (BMC) of C and C++ programs is challenging due to the complex and intricate syntax and semantics of these programming languages. The BMC tool LLBMC presented in this paper thus uses the LLVM compiler framework in order to translate C and C++ programs into LLVM's intermediate representation. The resulting code is then converted into a logical representation and simplified using rewrite rules. The simplified formula is finally passed to an SMT solver. In contrast to many other tools, LLBMC uses a flat, bit-precise memory model. It can thus precisely model, e.g., memory-based re-interpret casts as used in C and static/dynamic casts as used in C++. An empirical evaluation shows that LLBMC compares favorably to the related BMC tools CBMC and ESBMC.

2011

  • Stephan Falke, Florian Merz, and Carsten Sinz:
    A Theory of C-Style Memory Allocation
    In Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT '11), Snowbird, USA
    This paper introduces the theory TH for reasoning about the correctness of memory access operations in the context of a C-style heap memory. The proposed approach makes a clear distinction between reasoning about the values stored in memory and checking whether access to a specific memory location is allowed. The theory provides support for malloc and free and is presented in the form of axioms that can be converted into conditional rewrite rules. It is also shown how TH can be used in a bounded model checker for C programs.

2010

  • Carsten Sinz, Stephan Falke, and Florian Merz:
    A Precise Memory Model for Low-Level Bounded Model Checking
    In Proceedings of the 5th International Workshop on Systems Software Verification (SSV '10), Vancouver, Canada
    Formalizing the semantics of programming languages like C or C++ for bounded model checking can be cumbersome if complete coverage of all language features is to be achieved. On the other hand, low-level languages that occur during translation (compilation) have a much simpler semantics since they are closer to the machine level. It thus makes sense to use these low-level languages for bounded model checking. In this paper we present a highly precise memory model suitable for bounded model checking of such low-level languages. Our method also takes memory protection (malloc/free) into account.