01724nam 2200373z- 450 9910346909903321202102111000020678(CKB)4920000000101423(oapen)https://directory.doabooks.org/handle/20.500.12854/48105(oapen)doab48105(EXLCZ)99492000000010142320202102d2011 |y 0engurmn|---annantxtrdacontentcrdamediacrrdacarrierFrom Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based SecurityKIT Scientific Publishing20111 online resource (XIX, 203 p. p.)3-86644-594-6 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.From Formal Semantics to Verified Slicing Formal SemanticsLanguage Based SecurityModularitySlicingTheorem ProvingWasserrab Danielauth1302950BOOK9910346909903321From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security3026762UNINA