KIT-Homepage
LLBMC — The Low-Level Bounded Model Checker
 
  • Introduction
  • News
  • Downloads
  • Usage
  • Publications
  • Presentations
  • Awards
  • Authors / Contact
New version (2013.1) of LLBMC available!

Presentations

2013

  • The Bounded Model Checker LLBMC (Tool Demonstration)
    Presented at the 28th International Conference on Automated Software Engineering (ASE '13)
  • Extending the Theory of Arrays: memset, memcpy, and Beyond
    Presented at the 5th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '13)

2012

  • A Theory of Arrays with Set and Copy Operations
    Presented at the 10th International Workshop on Satisfiability Modulo Theories (SMT '12)
  • LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR
    Presented at the 4th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '12)

2011

  • A Theory of C-Style Memory Allocation
    Presented at the 9th International Workshop on Satisfiability Modulo Theories (SMT '11)
  • LLBMC: The Low-Level Bounded Model Checker
    Presented as a Google Tech Talk at Google Munich

2010

  • The Low-Level Bounded Model Checker LLBMC: A Precise Memory Model for LLBMC
    Presented at the 5th International Workshop on Systems Software Verification (SSV '10)
  • Low-Level Software Bounded Model Checking: Fully Automatic Software Verification
    Presented at the Deduktionstreffen 2010
  • The Low-Level Bounded Model Checker LLBMC
    Presented at the 9th KeY Symposium 2010
This site is hosted by Karlsruhe Institute of Technology (KIT), Germany back to top