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.


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