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
Seitenaufrufe: 76
seit 14.05.2018
Downloads: 750
seit 04.06.2014
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Jahr 2013
Sprache Englisch
Identifikator urn:nbn:de:swb:90-411691
KITopen-ID: 1000041169
Verlag KIT, Karlsruhe
Abschlussart 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
Schlagworte verification, refinement, dynamic logic, interaction, intermediate language
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page