From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security

• Váldodahkki: Wasserrab, Daniel (auth)
• Materiálatiipa: Elektrovnnalaš Girjji oassi
• Giella: eaŋgalasgiella
• Almmustuhtton: KIT Scientific Publishing 2011
• Fáttát: Formal Semantics; Slicing; Theorem Proving; Language Based Security; Modularity
• Liŋkkat: DOAB: download the publication; DOAB: description of the publication

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