KIT | KIT-Bibliothek | Impressum | Datenschutz

From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security

Wasserrab, Daniel

Abstract:
This book presents a modular framework for slicing in the proof assistant Isabelle/HOL which is based on abstract control flow graphs. Building on such abstract structures renders the correctness results language-independent. To prove that they hold for a specific language, it remains to instantiate the framework with this language, which requires a formal semantics of this language in Isabelle/HOL. We show that formal semantics even for sophisticated high-level languages are realizable.

Open Access Logo


Volltext §
DOI: 10.5445/KSP/1000020678
Die gedruckte Version dieser Publikation können Sie hier kaufen.
Coverbild
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Hochschulschrift
Jahr 2011
Sprache Englisch
Identifikator ISBN: 978-3-86644-594-9
urn:nbn:de:0072-206780
KITopen-ID: 1000020678
Verlag KIT Scientific Publishing, Karlsruhe
Umfang XIX, 203 S.
Abschlussart Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Programmstrukturen und Datenorganisation (IPD)
Prüfungsdatum 19.10.2010
Referent/Betreuer Prof. G. Snelting
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
Schlagworte Theorem Proving, Formal Semantics, Slicing, Modularity, Language Based Security
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page