KIT | KIT-Bibliothek | Impressum
Open Access Logo
URN: urn:nbn:de:swb:90-411691

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

Ulbrich, Mattias

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.

Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Jahr 2013
Sprache Englisch
Identifikator KITopen ID: 1000041169
Verlag 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