KIT | KIT-Bibliothek | Impressum | Datenschutz

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.

Volltext §
DOI: 10.5445/IR/1000063835
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsjahr 2016
Sprache Englisch
Identifikator urn:nbn:de:swb:90-638350
KITopen-ID: 1000063835
Verlag Karlsruher Institut für Technologie (KIT)
Umfang X, 208 S.
Art der Arbeit Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdaten 29.01.2016
Referent/Betreuer Sinz, C.
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page