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...
- Autores:
- Tipo de recurso:
- Book
- Fecha de publicación:
- 2011
- Institución:
- Universidad de Bogotá Jorge Tadeo Lozano
- Repositorio:
- Expeditio: repositorio UTadeo
- Idioma:
- eng
- OAI Identifier:
- oai:expeditiorepositorio.utadeo.edu.co:20.500.12010/17577
- Acceso en línea:
- https://directory.doabooks.org/handle/20.500.12854/48105
http://hdl.handle.net/20.500.12010/17577
- Palabra clave:
- Formal Semantics
Slicing
Theorem Proving
Web semántica
Ontologías (Recuperación de información)
Redes semánticas (Teoría de la información)
- Rights
- License
- Abierto (Texto Completo)
| id |
UTADEO2_8f6f46c96531c58354a336c9d855e42f |
|---|---|
| oai_identifier_str |
oai:expeditiorepositorio.utadeo.edu.co:20.500.12010/17577 |
| network_acronym_str |
UTADEO2 |
| network_name_str |
Expeditio: repositorio UTadeo |
| repository_id_str |
|
| dc.title.spa.fl_str_mv |
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 |
| spellingShingle |
From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security Formal Semantics Slicing Theorem Proving Web semántica Ontologías (Recuperación de información) Redes semánticas (Teoría de la información) |
| title_short |
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_sort |
From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security |
| dc.subject.spa.fl_str_mv |
Formal Semantics Slicing Theorem Proving |
| topic |
Formal Semantics Slicing Theorem Proving Web semántica Ontologías (Recuperación de información) Redes semánticas (Teoría de la información) |
| dc.subject.lemb.spa.fl_str_mv |
Web semántica Ontologías (Recuperación de información) Redes semánticas (Teoría de la información) |
| 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. |
| publishDate |
2011 |
| dc.date.created.none.fl_str_mv |
2011 |
| dc.date.accessioned.none.fl_str_mv |
2021-02-22T17:29:30Z |
| dc.date.available.none.fl_str_mv |
2021-02-22T17:29:30Z |
| dc.type.coar.spa.fl_str_mv |
http://purl.org/coar/resource_type/c_2f33 |
| format |
http://purl.org/coar/resource_type/c_2f33 |
| dc.identifier.isbn.none.fl_str_mv |
9783866445949 |
| dc.identifier.other.none.fl_str_mv |
https://directory.doabooks.org/handle/20.500.12854/48105 |
| dc.identifier.uri.none.fl_str_mv |
http://hdl.handle.net/20.500.12010/17577 |
| dc.identifier.doi.none.fl_str_mv |
10.5445/KSP/1000020678 |
| identifier_str_mv |
9783866445949 10.5445/KSP/1000020678 |
| url |
https://directory.doabooks.org/handle/20.500.12854/48105 http://hdl.handle.net/20.500.12010/17577 |
| dc.language.iso.spa.fl_str_mv |
eng |
| language |
eng |
| dc.rights.coar.fl_str_mv |
http://purl.org/coar/access_right/c_abf2 |
| dc.rights.local.spa.fl_str_mv |
Abierto (Texto Completo) |
| dc.rights.creativecommons.none.fl_str_mv |
https://creativecommons.org/licenses/by-nc-nd/4.0/ |
| rights_invalid_str_mv |
Abierto (Texto Completo) https://creativecommons.org/licenses/by-nc-nd/4.0/ http://purl.org/coar/access_right/c_abf2 |
| dc.format.extent.spa.fl_str_mv |
XIX, 203 páginas |
| dc.format.mimetype.spa.fl_str_mv |
application/pdf |
| dc.publisher.spa.fl_str_mv |
KIT Scientific Publishing |
| institution |
Universidad de Bogotá Jorge Tadeo Lozano |
| bitstream.url.fl_str_mv |
https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17577/3/978-3-86644-594-9_pdfa.pdf.jpg https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17577/1/978-3-86644-594-9_pdfa.pdf https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17577/2/license.txt |
| bitstream.checksum.fl_str_mv |
64f707b417060144a669334e8085c6a2 9507a10808000c5f5ca3a29311d504cd abceeb1c943c50d3343516f9dbfc110f |
| bitstream.checksumAlgorithm.fl_str_mv |
MD5 MD5 MD5 |
| repository.name.fl_str_mv |
Repositorio Institucional - Universidad Jorge Tadeo Lozano |
| repository.mail.fl_str_mv |
expeditio@utadeo.edu.co |
| _version_ |
1814213937009262592 |
| spelling |
2021-02-22T17:29:30Z2021-02-22T17:29:30Z20119783866445949https://directory.doabooks.org/handle/20.500.12854/48105http://hdl.handle.net/20.500.12010/1757710.5445/KSP/1000020678This 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.XIX, 203 páginasapplication/pdfengKIT Scientific PublishingFormal SemanticsSlicingTheorem ProvingWeb semánticaOntologías (Recuperación de información)Redes semánticas (Teoría de la información)From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based SecurityAbierto (Texto Completo)https://creativecommons.org/licenses/by-nc-nd/4.0/http://purl.org/coar/access_right/c_abf2http://purl.org/coar/resource_type/c_2f33Wasserrab, DanielTHUMBNAIL978-3-86644-594-9_pdfa.pdf.jpg978-3-86644-594-9_pdfa.pdf.jpgIM Thumbnailimage/jpeg22118https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17577/3/978-3-86644-594-9_pdfa.pdf.jpg64f707b417060144a669334e8085c6a2MD53open accessORIGINAL978-3-86644-594-9_pdfa.pdf978-3-86644-594-9_pdfa.pdfVer documentoapplication/pdf9958709https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17577/1/978-3-86644-594-9_pdfa.pdf9507a10808000c5f5ca3a29311d504cdMD51open accessLICENSElicense.txtlicense.txttext/plain; charset=utf-82938https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17577/2/license.txtabceeb1c943c50d3343516f9dbfc110fMD52open access20.500.12010/17577oai:expeditiorepositorio.utadeo.edu.co:20.500.12010/175772021-02-22 12:30:28.343open accessRepositorio Institucional - Universidad Jorge Tadeo Lozanoexpeditio@utadeo.edu.coQXV0b3Jpem8gYWwgU2lzdGVtYSBkZSBCaWJsaW90ZWNhcyBVbml2ZXJzaWRhZCBkZSBCb2dvdMOhIEpvcmdlIFRhZGVvIExvemFubyBwYXJhIHF1ZSBjb24gZmluZXMgYWNhZMOpbWljb3MsIHByZXNlcnZlLCBjb25zZXJ2ZSwgb3JnYW5pY2UsIGVkaXRlIHkgbW9kaWZpcXVlIHRlY25vbMOzZ2ljYW1lbnRlIGVsIGRvY3VtZW50byBhbnRlcmlvcm1lbnRlIGNhcmdhZG8gYWwgUmVwb3NpdG9yaW8gSW5zdGl0dWNpb25hbCBFeHBlZGl0aW8KCkV4Y2VwdHVhbmRvIHF1ZSBlbCBkb2N1bWVudG8gc2VhIGNvbmZpZGVuY2lhbCwgYXV0b3Jpem8gYSB1c3VhcmlvcyBpbnRlcm5vcyB5IGV4dGVybm9zIGRlIGxhIEluc3RpdHVjacOzbiBhIGNvbnN1bHRhciB5IHJlcHJvZHVjaXIgZWwgY29udGVuaWRvIGRlbCBkb2N1bWVudG8gcGFyYSBmaW5lcyBhY2Fkw6ltaWNvcyBudW5jYSBwYXJhIHVzb3MgY29tZXJjaWFsZXMsIGN1YW5kbyBtZWRpYW50ZSBsYSBjb3JyZXNwb25kaWVudGUgY2l0YSBiaWJsaW9ncsOhZmljYSBzZSBsZSBkZSBjcsOpZGl0byBhIGxhIG9icmEgeSBzdShzKSBhdXRvcihzKS4KCkV4Y2VwdHVhbmRvIHF1ZSBlbCBkb2N1bWVudG8gc2VhIGNvbmZpZGVuY2lhbCwgYXV0b3Jpem8gYXBsaWNhciBsYSBsaWNlbmNpYSBkZWwgZXN0w6FuZGFyIGludGVybmFjaW9uYWwgQ3JlYXRpdmUgQ29tbW9ucyAoQXR0cmlidXRpb24tTm9uQ29tbWVyY2lhbC1Ob0Rlcml2YXRpdmVzIDQuMCBJbnRlcm5hdGlvbmFsKSBxdWUgaW5kaWNhIHF1ZSBjdWFscXVpZXIgcGVyc29uYSBwdWVkZSB1c2FyIGxhIG9icmEgZGFuZG8gY3LDqWRpdG8gYWwgYXV0b3IsIHNpbiBwb2RlciBjb21lcmNpYXIgY29uIGxhIG9icmEgeSBzaW4gZ2VuZXJhciBvYnJhcyBkZXJpdmFkYXMuCgpFbCAobG9zKSBhdXRvcihlcykgY2VydGlmaWNhKG4pIHF1ZSBlbCBkb2N1bWVudG8gbm8gaW5mcmluZ2UgbmkgYXRlbnRhIGNvbnRyYSBkZXJlY2hvcyBpbmR1c3RyaWFsZXMsIHBhdHJpbW9uaWFsZXMsIGludGVsZWN0dWFsZXMsIG1vcmFsZXMgbyBjdWFscXVpZXIgb3RybyBkZSB0ZXJjZXJvcywgYXPDrSBtaXNtbyBkZWNsYXJhbiBxdWUgbGEgVW5pdmVyc2lkYWQgSm9yZ2UgVGFkZW8gTG96YW5vIHNlIGVuY3VlbnRyYSBsaWJyZSBkZSB0b2RhIHJlc3BvbnNhYmlsaWRhZCBjaXZpbCwgYWRtaW5pc3RyYXRpdmEgeS9vIHBlbmFsIHF1ZSBwdWVkYSBkZXJpdmFyc2UgZGUgbGEgcHVibGljYWNpw7NuIGRlbCB0cmFiYWpvIGRlIGdyYWRvIHkvbyB0ZXNpcyBlbiBjYWxpZGFkIGRlIGFjY2VzbyBhYmllcnRvIHBvciBjdWFscXVpZXIgbWVkaW8uCgpFbiBjdW1wbGltaWVudG8gY29uIGxvIGRpc3B1ZXN0byBlbiBsYSBMZXkgMTU4MSBkZSAyMDEyIHkgZXNwZWNpYWxtZW50ZSBlbiB2aXJ0dWQgZGUgbG8gZGlzcHVlc3RvIGVuIGVsIEFydMOtY3VsbyAxMCBkZWwgRGVjcmV0byAxMzc3IGRlIDIwMTMsIGF1dG9yaXpvIGEgbGEgVW5pdmVyc2lkYWQgSm9yZ2UgVGFkZW8gTG96YW5vIGEgcHJvY2VkZXIgY29uIGVsIHRyYXRhbWllbnRvIGRlIGxvcyBkYXRvcyBwZXJzb25hbGVzIHBhcmEgZmluZXMgYWNhZMOpbWljb3MsIGhpc3TDs3JpY29zLCBlc3RhZMOtc3RpY29zIHkgYWRtaW5pc3RyYXRpdm9zIGRlIGxhIEluc3RpdHVjacOzbi4gRGUgY29uZm9ybWlkYWQgY29uIGxvIGVzdGFibGVjaWRvIGVuIGVsIGFydMOtY3VsbyAzMCBkZSBsYSBMZXkgMjMgZGUgMTk4MiB5IGVsIGFydMOtY3VsbyAxMSBkZSBsYSBEZWNpc2nDs24gQW5kaW5hIDM1MSBkZSAxOTkzLCBhY2xhcmFtb3MgcXVlIOKAnExvcyBkZXJlY2hvcyBtb3JhbGVzIHNvYnJlIGVsIHRyYWJham8gc29uIHByb3BpZWRhZCBkZSBsb3MgYXV0b3Jlc+KAnSwgbG9zIGN1YWxlcyBzb24gaXJyZW51bmNpYWJsZXMsIGltcHJlc2NyaXB0aWJsZXMsIGluZW1iYXJnYWJsZXMgZSBpbmFsaWVuYWJsZXMuCgpDb24gZWwgcmVnaXN0cm8gZW4gbGEgcMOhZ2luYSwgYXV0b3Jpem8gZGUgbWFuZXJhIGV4cHJlc2EgYSBsYSBGVU5EQUNJw5NOIFVOSVZFUlNJREFEIERFIEJPR09Uw4EgSk9SR0UgVEFERU8gTE9aQU5PLCBlbCB0cmF0YW1pZW50byBkZSBtaXMgZGF0b3MgcGVyc29uYWxlcyBwYXJhIHByb2Nlc2FyIG8gY29uc2VydmFyLCBjb24gZmluZXMgZXN0YWTDrXN0aWNvcywgZGUgY29udHJvbCBvIHN1cGVydmlzacOzbiwgYXPDrSBjb21vIHBhcmEgZWwgZW52w61vIGRlIGluZm9ybWFjacOzbiB2w61hIGNvcnJlbyBlbGVjdHLDs25pY28sIGRlbnRybyBkZWwgbWFyY28gZXN0YWJsZWNpZG8gcG9yIGxhIExleSAxNTgxIGRlIDIwMTIgeSBzdXMgZGVjcmV0b3MgY29tcGxlbWVudGFyaW9zIHNvYnJlIFRyYXRhbWllbnRvIGRlIERhdG9zIFBlcnNvbmFsZXMuIEVuIGN1YWxxdWllciBjYXNvLCBlbnRpZW5kbyBxdWUgcG9kcsOpIGhhY2VyIHVzbyBkZWwgZGVyZWNobyBhIGNvbm9jZXIsIGFjdHVhbGl6YXIsIHJlY3RpZmljYXIgbyBzdXByaW1pciBsb3MgZGF0b3MgcGVyc29uYWxlcyBtZWRpYW50ZSBlbCBlbnbDrW8gZGUgdW5hIGNvbXVuaWNhY2nDs24gZXNjcml0YSBhbCBjb3JyZW8gZWxlY3Ryw7NuaWNvIHByb3RlY2Npb25kYXRvc0B1dGFkZW8uZWR1LmNvLgoKTGEgRlVOREFDScOTTiBVTklWRVJTSURBRCBERSBCT0dPVMOBIEpPUkdFIFRBREVPIExPWkFOTyBubyB1dGlsaXphcsOhIGxvcyBkYXRvcyBwZXJzb25hbGVzIHBhcmEgZmluZXMgZGlmZXJlbnRlcyBhIGxvcyBhbnVuY2lhZG9zIHkgZGFyw6EgdW4gdXNvIGFkZWN1YWRvIHkgcmVzcG9uc2FibGUgYSBzdXMgZGF0b3MgcGVyc29uYWxlcyBkZSBhY3VlcmRvIGNvbiBsYSBkaXJlY3RyaXogZGUgUHJvdGVjY2nDs24gZGUgRGF0b3MgUGVyc29uYWxlcyBxdWUgcG9kcsOhIGNvbnN1bHRhciBlbjogaHR0cDovL3d3dy51dGFkZW8uZWR1LmNvL2VzL2xpbmsvZGVzY3VicmUtbGEtdW5pdmVyc2lkYWQvMi9kb2N1bWVudG9zCg== |