KIT | KIT-Bibliothek | Impressum

Theory and Implementation of Software Bounded Model Checking

Merz, Florian

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.

Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Jahr 2016
Sprache Englisch
Identifikator DOI(KIT): 10.5445/IR/1000063835
URN: urn:nbn:de:swb:90-638350
KITopen ID: 1000063835
Verlag Karlsruhe
Umfang X, 208 S.
Abschlussart Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdaten 29.01.2016
Referent/Betreuer Dr. C. Sinz
Lizenz CC BY-SA 3.0 DE: Creative Commons Namensnennung – Weitergabe unter gleichen Bedingungen 3.0 Deutschland
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page