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

• Glavni autor: Wasserrab, Daniel (auth)
• Format: Elektronički Poglavlje knjige
• Jezik: engleski
• Izdano: KIT Scientific Publishing 2011
• Teme: Formal Semantics; Slicing; Theorem Proving; Language Based Security; Modularity
• Online pristup: 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...