Reasoning about Abstract State Machines: The WAM Case Study
| dc.creator | Schellhorn,Gerhard | |
| dc.creator | Ahrendt,Wolfgang | |
| dc.date | 1997 | |
| dc.date.accessioned | 2024-02-06T12:48:47Z | |
| dc.date.available | 2024-02-06T12:48:47Z | |
| dc.description | This paper describes the first half of the formal verification of a Prolog compiler with the KIV ("Karlsruhe Interactive Verifier") system. Our work is based on [BR95], where an operational Prolog semantics is defined using the formalism of Gurevich Abstract State Machines, and then refined in several steps to the Warren Abstract Machine (WAM). We define a general translation of sequential Abstract State Machines to Dynamic Logic, which formalizes correctness of such refinement steps as a deduction problem. A proof technique for verification is presented, which corresponds to the informal use of proof maps. 6 of the 12 given refinement steps were verified. We found that the proof sketches given in [BR95] hide a lot of implicit assumptions. We report on our experiences in uncovering these assumptions incrementally during formal verification, and the support KIV offers for such `evolutionary' correctness proofs. | |
| dc.format | text/html | |
| dc.identifier | https://doi.org/10.3217/jucs-003-04-0377 | |
| dc.identifier | https://lib.jucs.org/article/27353/ | |
| dc.identifier.uri | https://openrepository.mephi.ru/handle/123456789/7143 | |
| dc.language | en | |
| dc.publisher | Journal of Universal Computer Science | |
| dc.relation | info:eu-repo/semantics/altIdentifier/eissn/0948-6968 | |
| dc.relation | info:eu-repo/semantics/altIdentifier/pissn/0948-695X | |
| dc.rights | info:eu-repo/semantics/openAccess | |
| dc.rights | J.UCS License | |
| dc.source | JUCS - Journal of Universal Computer Science 3(4): 377-413 | |
| dc.title | Reasoning about Abstract State Machines: The WAM Case Study | |
| dc.type | Research Article |