From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security
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. |