LEADER 01724nam  2200373z- 450 
001 9910346909903321
005 20210211
010   $a1000020678
035   $a(CKB)4920000000101423
035   $a(oapen)https://directory.doabooks.org/handle/20.500.12854/48105
035   $a(oapen)doab48105
035   $a(EXLCZ)994920000000101423
100   $a20202102d2011      |y         0
101 0 $aeng
135   $aurmn|---annan
181   $ctxt$2rdacontent
182   $cc$2rdamedia
183   $acr$2rdacarrier
200 00$aFrom Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security
210   $cKIT Scientific Publishing$d2011
215   $a1 online resource (XIX, 203 p. p.)
311 08$a3-86644-594-6 
330   $aThis 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.
517   $aFrom Formal Semantics to Verified Slicing 
610   $aFormal Semantics
610   $aLanguage Based Security
610   $aModularity
610   $aSlicing
610   $aTheorem Proving
700   $aWasserrab$b Daniel$4auth$01302950
906   $aBOOK
912   $a9910346909903321
996   $aFrom Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security$93026762
997   $aUNINA