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...
-д хадгалсан:
| Үндсэн зохиолч: | |
|---|---|
| Формат: | Online |
| Хэл сонгох: | англи |
| Хэвлэсэн: |
KIT Scientific Publishing
2021
|
| Нөхцлүүд: | |
| Онлайн хандалт: | 35259 |
| Шошгууд: |
Шошго байхгүй, Энэхүү баримтыг шошголох эхний хүн болох!
|
| _version_ | 1869521762798010368 |
|---|---|
| author | Weiß, Benjamin |
| author_browse | Weiß, Benjamin |
| author_facet | Weiß, Benjamin |
| author_sort | Weiß, Benjamin |
| collection | Directory of Open Access Books |
| 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. |
| format | Online |
| id | doab-20.500.12854ir-44626 |
| 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-446262023-12-20T18:40:46Z Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction Weiß, Benjamin QA75.5-76.95 design by contract software specification software verification abstract interpretation theorem proving bic Book Industry Communication::U Computing & information technology::UY Computer science 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. 2021-02-11T11:03:05Z 2021-02-11T11:03:05Z 2019-07-30 20:02:01 2011 book 35259 9783866446236 https://directory.doabooks.org/handle/20.500.12854/44626 eng image/jpeg Attribution-NonCommercial-NoDerivatives 4.0 International https://www.ksp.kit.edu/9783866446236 KIT Scientific Publishing 10.5445/KSP/1000021694 10.5445/KSP/1000021694 68fffc18-8f7b-44fa-ac7e-0b7d7d979bd2 9783866446236 xxi, 269 p. open access |
| spellingShingle | QA75.5-76.95 design by contract software specification software verification abstract interpretation theorem proving bic Book Industry Communication::U Computing & information technology::UY Computer science Weiß, Benjamin 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 |
| 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_short | 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 |
| topic | QA75.5-76.95 design by contract software specification software verification abstract interpretation theorem proving bic Book Industry Communication::U Computing & information technology::UY Computer science |
| topic_facet | QA75.5-76.95 design by contract software specification software verification abstract interpretation theorem proving bic Book Industry Communication::U Computing & information technology::UY Computer science |
| url | 35259 |
| work_keys_str_mv | AT weißbenjamin deductiveverificationofobjectorientedsoftwaredynamicframesdynamiclogicandpredicateabstraction |