KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo
DOI: 10.5445/IR/1000063835

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 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
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page