KIT | KIT-Bibliothek | Impressum | Datenschutz

Dynamic Logic for an Intermediate Language: Verification, Interaction and Refinement

Ulbrich, Mattias

Abstract:
This thesis is about ensuring that software behaves as it is supposed to behave. More precisely, it is concerned with the deductive verification of the compliance of software implementations with their formal specification. Two successful ideas in program verification are integrated into a new approach: dynamic logic and intermediate verification language. The well-established technique of refinement is used to decompose the difficult task of program verification into two easier tasks.

Open Access Logo


Volltext §
DOI: 10.5445/IR/1000041169
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsjahr 2013
Sprache Englisch
Identifikator urn:nbn:de:swb:90-411691
KITopen-ID: 1000041169
Verlag KIT, Karlsruhe
Art der Arbeit Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdaten 17.06.2013
Referent/Betreuer Prof. P. H. Schmitt
Schlagwörter verification, refinement, dynamic logic, interaction, intermediate language
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page