KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo
§
Volltext
DOI: 10.5445/KSP/1000020678
Die gedruckte Version dieser Publikation können Sie hier kaufen.

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.


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: 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