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.

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.

Volltext §
DOI: 10.5445/KSP/1000020678
Seitenaufrufe: 335
seit 24.05.2018
Downloads: 3217
seit 30.03.2011
Die gedruckte Version dieser Publikation können Sie hier kaufen.
Cover der Publikation
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page