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.
Umfang: XIX, 203 S.
Preis: €37.00 | £34.00 | $65.00
These are words or phrases in the text that have been automatically identified by the Named Entity Recognition and Disambiguation service, which provides Wikipedia () and Wikidata () links for these entities.
Wasserrab, D. 2011. From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security. Karlsruhe: KIT Scientific Publishing. DOI: https://doi.org/10.5445/KSP/1000020678
Dieses Buch ist lizenziert unter Creative Commons Attribution + Noncommercial + NoDerivatives 3.0 DE Dedication
Dieses Buch ist Peer reviewed. Informationen dazu finden Sie hier
Veröffentlicht am 30. März 2011
Englisch
223
Paperback | 978-3-86644-594-9 |