Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 3 / Issue 4

available in:   PDF (406 kB) PS (154 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-003-04-0377


Reasoning about Abstract State Machines: The WAM Case Study

Gerhard Schellhorn (Abt. Programmiermethodik, Universität Ulm, Germany)

Wolfgang Ahrendt (Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, Germany)

Abstract: 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.