KIT | KIT-Bibliothek | Impressum | Datenschutz

Advancing Deductive Program-Level Verification for Real-World Application: Lessons Learned from an Industrial Case Study

Bormer, Thorsten

This thesis is concerned with practicability of deductive program verification on source code level. As part of a case study for the verification of real-world software, the specification and verification approach to show correctness of the virtualizing kernel PikeOS is presented. Issues within the verification process using current tools and methodologies are discussed and several aspects of these problems are then addressed in detail to improve the verification process and tool usability.

Open Access Logo

Volltext §
DOI: 10.5445/IR/1000049792
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsjahr 2014
Sprache Englisch
Identifikator urn:nbn:de:swb:90-497927
KITopen-ID: 1000049792
Verlag KIT, Karlsruhe
Art der Arbeit Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdaten 23.10.2014
Referent/Betreuer Prof. B. Beckert
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page