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...
Saved in:
: | |
---|---|
Year of Publication: | 2011 |
Language: | English |
Physical Description: | 1 electronic resource (XIX, 203 p. p.) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
993545262504498 |
---|---|
ctrlnum |
(CKB)4920000000101423 (oapen)https://directory.doabooks.org/handle/20.500.12854/48105 (EXLCZ)994920000000101423 |
collection |
bib_alma |
record_format |
marc |
spelling |
Wasserrab, Daniel auth From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security From Formal Semantics to Verified Slicing KIT Scientific Publishing 2011 1 electronic resource (XIX, 203 p. p.) text txt rdacontent computer c rdamedia online resource cr rdacarrier 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. English Formal Semantics Slicing Theorem Proving Language Based Security Modularity 3-86644-594-6 |
language |
English |
format |
eBook |
author |
Wasserrab, Daniel |
spellingShingle |
Wasserrab, Daniel From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
author_facet |
Wasserrab, Daniel |
author_variant |
d w dw |
author_sort |
Wasserrab, Daniel |
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_auth |
From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
title_alt |
From Formal Semantics to Verified Slicing |
title_new |
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 |
publisher |
KIT Scientific Publishing |
publishDate |
2011 |
physical |
1 electronic resource (XIX, 203 p. p.) |
isbn |
1000020678 3-86644-594-6 |
illustrated |
Not Illustrated |
work_keys_str_mv |
AT wasserrabdaniel fromformalsemanticstoverifiedslicingamodularframeworkwithapplicationsinlanguagebasedsecurity AT wasserrabdaniel fromformalsemanticstoverifiedslicing |
status_str |
n |
ids_txt_mv |
(CKB)4920000000101423 (oapen)https://directory.doabooks.org/handle/20.500.12854/48105 (EXLCZ)994920000000101423 |
carrierType_str_mv |
cr |
is_hierarchy_title |
From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
_version_ |
1787548485924421632 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>01553nam-a2200337z--4500</leader><controlfield tag="001">993545262504498</controlfield><controlfield tag="005">20231214132923.0</controlfield><controlfield tag="006">m o d </controlfield><controlfield tag="007">cr|mn|---annan</controlfield><controlfield tag="008">202102s2011 xx |||||o ||| 0|eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">1000020678</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(CKB)4920000000101423</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(oapen)https://directory.doabooks.org/handle/20.500.12854/48105</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(EXLCZ)994920000000101423</subfield></datafield><datafield tag="041" ind1="0" ind2=" "><subfield code="a">eng</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Wasserrab, Daniel</subfield><subfield code="4">auth</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security</subfield></datafield><datafield tag="246" ind1=" " ind2=" "><subfield code="a">From Formal Semantics to Verified Slicing </subfield></datafield><datafield tag="260" ind1=" " ind2=" "><subfield code="b">KIT Scientific Publishing</subfield><subfield code="c">2011</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 electronic resource (XIX, 203 p. p.)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="520" ind1=" " ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="546" ind1=" " ind2=" "><subfield code="a">English</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Formal Semantics</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Slicing</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Theorem Proving</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Language Based Security</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Modularity</subfield></datafield><datafield tag="776" ind1=" " ind2=" "><subfield code="z">3-86644-594-6</subfield></datafield><datafield tag="906" ind1=" " ind2=" "><subfield code="a">BOOK</subfield></datafield><datafield tag="ADM" ind1=" " ind2=" "><subfield code="b">2023-12-15 05:35:43 Europe/Vienna</subfield><subfield code="f">system</subfield><subfield code="c">marc21</subfield><subfield code="a">2019-11-10 04:18:40 Europe/Vienna</subfield><subfield code="g">false</subfield></datafield><datafield tag="AVE" ind1=" " ind2=" "><subfield code="i">DOAB Directory of Open Access Books</subfield><subfield code="P">DOAB Directory of Open Access Books</subfield><subfield code="x">https://eu02.alma.exlibrisgroup.com/view/uresolver/43ACC_OEAW/openurl?u.ignore_date_coverage=true&portfolio_pid=5337861340004498&Force_direct=true</subfield><subfield code="Z">5337861340004498</subfield><subfield code="b">Available</subfield><subfield code="8">5337861340004498</subfield></datafield></record></collection> |