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

• Main Author: Wasserrab, Daniel (auth)
• Format: Electronic Book Chapter
• Language: English
• Published: KIT Scientific Publishing 2011
• Subjects: Formal Semantics; Slicing; Theorem Proving; Language Based Security; Modularity
• Online Access: 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...