The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV 
----------------------------------------------------------------------

Gerhard Schellhorn, Wolfgang Ahrendt


This chapter describes the first half of the formal, machine-supported
verification of a Prolog compiler with the KIV system.

Our work is based on the mathematical analysis given in (Boerger and
Rosenzweig, 1995), where an operational semantics (an "interpreter")
for Prolog is defined as an Abstract State Machine (ASM). This
interpreter is then transformed in 12 systematic refinements to an ASM
which executes machine code of the Warren Abstract Machine (WAM). The
goal of our case study was to formalize ASMs and the proof techniques
given in (Boerger and Rosenzweig, 1995), and to give machine checked
proofs for the correctness of the refinements. So far we have verified
the first 6 refinements, and we will give a detailed account on the
problems we found in verification.