Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction
Software systems play a central role in modern society, and their correctness is often crucially important. Formal specification and verification are promising approaches for ensuring correctness more rigorously than just by testing. This work presents an approach for deductively verifying design-by...
- 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/17576
- Acceso en línea:
- https://directory.doabooks.org/handle/20.500.12854/44626
http://hdl.handle.net/20.500.12010/17576
- Palabra clave:
- Design by contract
Software specification
Software verification
Arquitectura de software
Desarrollo de software
Ingeniería de software
- Rights
- License
- Abierto (Texto Completo)
| id |
UTADEO2_6702c30e0d416d6031f404b5b6772fa4 |
|---|---|
| oai_identifier_str |
oai:expeditiorepositorio.utadeo.edu.co:20.500.12010/17576 |
| network_acronym_str |
UTADEO2 |
| network_name_str |
Expeditio: repositorio UTadeo |
| repository_id_str |
|
| dc.title.spa.fl_str_mv |
Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction |
| title |
Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction |
| spellingShingle |
Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction Design by contract Software specification Software verification Arquitectura de software Desarrollo de software Ingeniería de software |
| title_short |
Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction |
| title_full |
Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction |
| title_fullStr |
Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction |
| title_full_unstemmed |
Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction |
| title_sort |
Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction |
| dc.subject.spa.fl_str_mv |
Design by contract Software specification Software verification |
| topic |
Design by contract Software specification Software verification Arquitectura de software Desarrollo de software Ingeniería de software |
| dc.subject.lemb.spa.fl_str_mv |
Arquitectura de software Desarrollo de software Ingeniería de software |
| description |
Software systems play a central role in modern society, and their correctness is often crucially important. Formal specification and verification are promising approaches for ensuring correctness more rigorously than just by testing. This work presents an approach for deductively verifying design-by-contract specifications of object-oriented programs. The approach is based on dynamic logic, and addresses the challenges of modularity and automation using dynamic frames and predicate abstraction. |
| publishDate |
2011 |
| dc.date.created.none.fl_str_mv |
2011 |
| dc.date.accessioned.none.fl_str_mv |
2021-02-22T17:24:18Z |
| dc.date.available.none.fl_str_mv |
2021-02-22T17:24:18Z |
| 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 |
9783866446236 |
| dc.identifier.other.none.fl_str_mv |
https://directory.doabooks.org/handle/20.500.12854/44626 |
| dc.identifier.uri.none.fl_str_mv |
http://hdl.handle.net/20.500.12010/17576 |
| dc.identifier.doi.none.fl_str_mv |
10.5445/KSP/1000021694 |
| identifier_str_mv |
9783866446236 10.5445/KSP/1000021694 |
| url |
https://directory.doabooks.org/handle/20.500.12854/44626 http://hdl.handle.net/20.500.12010/17576 |
| 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 |
xxi, 269 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/17576/1/978-3-86644-623-6_pdfa.pdf https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17576/2/license.txt https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17576/3/978-3-86644-623-6_pdfa.pdf.jpg |
| bitstream.checksum.fl_str_mv |
486fb80eb1f0dc6f212e309f79a1a088 abceeb1c943c50d3343516f9dbfc110f 9b387cd7a195131124c7d7a208cb811c |
| 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_ |
1814213818733035520 |
| spelling |
2021-02-22T17:24:18Z2021-02-22T17:24:18Z20119783866446236https://directory.doabooks.org/handle/20.500.12854/44626http://hdl.handle.net/20.500.12010/1757610.5445/KSP/1000021694Software systems play a central role in modern society, and their correctness is often crucially important. Formal specification and verification are promising approaches for ensuring correctness more rigorously than just by testing. This work presents an approach for deductively verifying design-by-contract specifications of object-oriented programs. The approach is based on dynamic logic, and addresses the challenges of modularity and automation using dynamic frames and predicate abstraction.xxi, 269 páginasapplication/pdfengKIT Scientific PublishingDesign by contractSoftware specificationSoftware verificationArquitectura de softwareDesarrollo de softwareIngeniería de softwareDeductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstractionAbierto (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_2f33Weiß, BenjaminORIGINAL978-3-86644-623-6_pdfa.pdf978-3-86644-623-6_pdfa.pdfVer documentoapplication/pdf13584815https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17576/1/978-3-86644-623-6_pdfa.pdf486fb80eb1f0dc6f212e309f79a1a088MD51open accessLICENSElicense.txtlicense.txttext/plain; charset=utf-82938https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17576/2/license.txtabceeb1c943c50d3343516f9dbfc110fMD52open accessTHUMBNAIL978-3-86644-623-6_pdfa.pdf.jpg978-3-86644-623-6_pdfa.pdf.jpgIM Thumbnailimage/jpeg11701https://expeditiorepositorio.utadeo.edu.co/bitstream/20.500.12010/17576/3/978-3-86644-623-6_pdfa.pdf.jpg9b387cd7a195131124c7d7a208cb811cMD53open access20.500.12010/17576oai:expeditiorepositorio.utadeo.edu.co:20.500.12010/175762021-02-22 12:25:32.137open accessRepositorio Institucional - Universidad Jorge Tadeo Lozanoexpeditio@utadeo.edu.coQXV0b3Jpem8gYWwgU2lzdGVtYSBkZSBCaWJsaW90ZWNhcyBVbml2ZXJzaWRhZCBkZSBCb2dvdMOhIEpvcmdlIFRhZGVvIExvemFubyBwYXJhIHF1ZSBjb24gZmluZXMgYWNhZMOpbWljb3MsIHByZXNlcnZlLCBjb25zZXJ2ZSwgb3JnYW5pY2UsIGVkaXRlIHkgbW9kaWZpcXVlIHRlY25vbMOzZ2ljYW1lbnRlIGVsIGRvY3VtZW50byBhbnRlcmlvcm1lbnRlIGNhcmdhZG8gYWwgUmVwb3NpdG9yaW8gSW5zdGl0dWNpb25hbCBFeHBlZGl0aW8KCkV4Y2VwdHVhbmRvIHF1ZSBlbCBkb2N1bWVudG8gc2VhIGNvbmZpZGVuY2lhbCwgYXV0b3Jpem8gYSB1c3VhcmlvcyBpbnRlcm5vcyB5IGV4dGVybm9zIGRlIGxhIEluc3RpdHVjacOzbiBhIGNvbnN1bHRhciB5IHJlcHJvZHVjaXIgZWwgY29udGVuaWRvIGRlbCBkb2N1bWVudG8gcGFyYSBmaW5lcyBhY2Fkw6ltaWNvcyBudW5jYSBwYXJhIHVzb3MgY29tZXJjaWFsZXMsIGN1YW5kbyBtZWRpYW50ZSBsYSBjb3JyZXNwb25kaWVudGUgY2l0YSBiaWJsaW9ncsOhZmljYSBzZSBsZSBkZSBjcsOpZGl0byBhIGxhIG9icmEgeSBzdShzKSBhdXRvcihzKS4KCkV4Y2VwdHVhbmRvIHF1ZSBlbCBkb2N1bWVudG8gc2VhIGNvbmZpZGVuY2lhbCwgYXV0b3Jpem8gYXBsaWNhciBsYSBsaWNlbmNpYSBkZWwgZXN0w6FuZGFyIGludGVybmFjaW9uYWwgQ3JlYXRpdmUgQ29tbW9ucyAoQXR0cmlidXRpb24tTm9uQ29tbWVyY2lhbC1Ob0Rlcml2YXRpdmVzIDQuMCBJbnRlcm5hdGlvbmFsKSBxdWUgaW5kaWNhIHF1ZSBjdWFscXVpZXIgcGVyc29uYSBwdWVkZSB1c2FyIGxhIG9icmEgZGFuZG8gY3LDqWRpdG8gYWwgYXV0b3IsIHNpbiBwb2RlciBjb21lcmNpYXIgY29uIGxhIG9icmEgeSBzaW4gZ2VuZXJhciBvYnJhcyBkZXJpdmFkYXMuCgpFbCAobG9zKSBhdXRvcihlcykgY2VydGlmaWNhKG4pIHF1ZSBlbCBkb2N1bWVudG8gbm8gaW5mcmluZ2UgbmkgYXRlbnRhIGNvbnRyYSBkZXJlY2hvcyBpbmR1c3RyaWFsZXMsIHBhdHJpbW9uaWFsZXMsIGludGVsZWN0dWFsZXMsIG1vcmFsZXMgbyBjdWFscXVpZXIgb3RybyBkZSB0ZXJjZXJvcywgYXPDrSBtaXNtbyBkZWNsYXJhbiBxdWUgbGEgVW5pdmVyc2lkYWQgSm9yZ2UgVGFkZW8gTG96YW5vIHNlIGVuY3VlbnRyYSBsaWJyZSBkZSB0b2RhIHJlc3BvbnNhYmlsaWRhZCBjaXZpbCwgYWRtaW5pc3RyYXRpdmEgeS9vIHBlbmFsIHF1ZSBwdWVkYSBkZXJpdmFyc2UgZGUgbGEgcHVibGljYWNpw7NuIGRlbCB0cmFiYWpvIGRlIGdyYWRvIHkvbyB0ZXNpcyBlbiBjYWxpZGFkIGRlIGFjY2VzbyBhYmllcnRvIHBvciBjdWFscXVpZXIgbWVkaW8uCgpFbiBjdW1wbGltaWVudG8gY29uIGxvIGRpc3B1ZXN0byBlbiBsYSBMZXkgMTU4MSBkZSAyMDEyIHkgZXNwZWNpYWxtZW50ZSBlbiB2aXJ0dWQgZGUgbG8gZGlzcHVlc3RvIGVuIGVsIEFydMOtY3VsbyAxMCBkZWwgRGVjcmV0byAxMzc3IGRlIDIwMTMsIGF1dG9yaXpvIGEgbGEgVW5pdmVyc2lkYWQgSm9yZ2UgVGFkZW8gTG96YW5vIGEgcHJvY2VkZXIgY29uIGVsIHRyYXRhbWllbnRvIGRlIGxvcyBkYXRvcyBwZXJzb25hbGVzIHBhcmEgZmluZXMgYWNhZMOpbWljb3MsIGhpc3TDs3JpY29zLCBlc3RhZMOtc3RpY29zIHkgYWRtaW5pc3RyYXRpdm9zIGRlIGxhIEluc3RpdHVjacOzbi4gRGUgY29uZm9ybWlkYWQgY29uIGxvIGVzdGFibGVjaWRvIGVuIGVsIGFydMOtY3VsbyAzMCBkZSBsYSBMZXkgMjMgZGUgMTk4MiB5IGVsIGFydMOtY3VsbyAxMSBkZSBsYSBEZWNpc2nDs24gQW5kaW5hIDM1MSBkZSAxOTkzLCBhY2xhcmFtb3MgcXVlIOKAnExvcyBkZXJlY2hvcyBtb3JhbGVzIHNvYnJlIGVsIHRyYWJham8gc29uIHByb3BpZWRhZCBkZSBsb3MgYXV0b3Jlc+KAnSwgbG9zIGN1YWxlcyBzb24gaXJyZW51bmNpYWJsZXMsIGltcHJlc2NyaXB0aWJsZXMsIGluZW1iYXJnYWJsZXMgZSBpbmFsaWVuYWJsZXMuCgpDb24gZWwgcmVnaXN0cm8gZW4gbGEgcMOhZ2luYSwgYXV0b3Jpem8gZGUgbWFuZXJhIGV4cHJlc2EgYSBsYSBGVU5EQUNJw5NOIFVOSVZFUlNJREFEIERFIEJPR09Uw4EgSk9SR0UgVEFERU8gTE9aQU5PLCBlbCB0cmF0YW1pZW50byBkZSBtaXMgZGF0b3MgcGVyc29uYWxlcyBwYXJhIHByb2Nlc2FyIG8gY29uc2VydmFyLCBjb24gZmluZXMgZXN0YWTDrXN0aWNvcywgZGUgY29udHJvbCBvIHN1cGVydmlzacOzbiwgYXPDrSBjb21vIHBhcmEgZWwgZW52w61vIGRlIGluZm9ybWFjacOzbiB2w61hIGNvcnJlbyBlbGVjdHLDs25pY28sIGRlbnRybyBkZWwgbWFyY28gZXN0YWJsZWNpZG8gcG9yIGxhIExleSAxNTgxIGRlIDIwMTIgeSBzdXMgZGVjcmV0b3MgY29tcGxlbWVudGFyaW9zIHNvYnJlIFRyYXRhbWllbnRvIGRlIERhdG9zIFBlcnNvbmFsZXMuIEVuIGN1YWxxdWllciBjYXNvLCBlbnRpZW5kbyBxdWUgcG9kcsOpIGhhY2VyIHVzbyBkZWwgZGVyZWNobyBhIGNvbm9jZXIsIGFjdHVhbGl6YXIsIHJlY3RpZmljYXIgbyBzdXByaW1pciBsb3MgZGF0b3MgcGVyc29uYWxlcyBtZWRpYW50ZSBlbCBlbnbDrW8gZGUgdW5hIGNvbXVuaWNhY2nDs24gZXNjcml0YSBhbCBjb3JyZW8gZWxlY3Ryw7NuaWNvIHByb3RlY2Npb25kYXRvc0B1dGFkZW8uZWR1LmNvLgoKTGEgRlVOREFDScOTTiBVTklWRVJTSURBRCBERSBCT0dPVMOBIEpPUkdFIFRBREVPIExPWkFOTyBubyB1dGlsaXphcsOhIGxvcyBkYXRvcyBwZXJzb25hbGVzIHBhcmEgZmluZXMgZGlmZXJlbnRlcyBhIGxvcyBhbnVuY2lhZG9zIHkgZGFyw6EgdW4gdXNvIGFkZWN1YWRvIHkgcmVzcG9uc2FibGUgYSBzdXMgZGF0b3MgcGVyc29uYWxlcyBkZSBhY3VlcmRvIGNvbiBsYSBkaXJlY3RyaXogZGUgUHJvdGVjY2nDs24gZGUgRGF0b3MgUGVyc29uYWxlcyBxdWUgcG9kcsOhIGNvbnN1bHRhciBlbjogaHR0cDovL3d3dy51dGFkZW8uZWR1LmNvL2VzL2xpbmsvZGVzY3VicmUtbGEtdW5pdmVyc2lkYWQvMi9kb2N1bWVudG9zCg== |