From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security
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...
Bewaard in:
| Hoofdauteur: | |
|---|---|
| Formaat: | Online |
| Taal: | Engels |
| Gepubliceerd in: |
KIT Scientific Publishing
2021
|
| Onderwerpen: | |
| Online toegang: | 35028 |
| Tags: |
Geen labels, Wees de eerste die dit record labelt!
|
| _version_ | 1869525638005653504 |
|---|---|
| author | Wasserrab, Daniel |
| author_browse | Wasserrab, Daniel |
| author_facet | Wasserrab, Daniel |
| author_sort | Wasserrab, Daniel |
| collection | Directory of Open Access Books |
| description | 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. |
| format | Online |
| id | doab-20.500.12854ir-48105 |
| institution | Directory of Open Access Books |
| language | eng |
| publishDate | 2021 |
| publishDateRange | 2021 |
| publishDateSort | 2021 |
| publisher | KIT Scientific Publishing |
| publisherStr | KIT Scientific Publishing |
| record_format | ojs |
| spelling | doab-20.500.12854ir-481052023-12-20T18:40:49Z From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security Wasserrab, Daniel QA75.5-76.95 Formal Semantics Slicing Theorem Proving Language Based Security Modularity bic Book Industry Communication::U Computing & information technology::UY Computer science 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. 2021-02-11T14:06:27Z 2021-02-11T14:06:27Z 2019-07-30 20:02:00 2011 book 35028 9783866445949 https://directory.doabooks.org/handle/20.500.12854/48105 eng image/jpeg Attribution-NonCommercial-NoDerivatives 4.0 International https://www.ksp.kit.edu/9783866445949 KIT Scientific Publishing 10.5445/KSP/1000020678 10.5445/KSP/1000020678 68fffc18-8f7b-44fa-ac7e-0b7d7d979bd2 9783866445949 XIX, 203 p. open access |
| spellingShingle | QA75.5-76.95 Formal Semantics Slicing Theorem Proving Language Based Security Modularity bic Book Industry Communication::U Computing & information technology::UY Computer science Wasserrab, Daniel From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
| title | From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
| title_full | From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
| title_fullStr | From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
| title_full_unstemmed | From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
| title_short | From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
| title_sort | from formal semantics to verified slicing a modular framework with applications in language based security |
| topic | QA75.5-76.95 Formal Semantics Slicing Theorem Proving Language Based Security Modularity bic Book Industry Communication::U Computing & information technology::UY Computer science |
| topic_facet | QA75.5-76.95 Formal Semantics Slicing Theorem Proving Language Based Security Modularity bic Book Industry Communication::U Computing & information technology::UY Computer science |
| url | 35028 |
| work_keys_str_mv | AT wasserrabdaniel fromformalsemanticstoverifiedslicingamodularframeworkwithapplicationsinlanguagebasedsecurity |