Proving WAM Compiler Correctness

In this note we analyse the proof of compiler correctness of the WAM given in the paper [Borger and Rosenzweig 92] with regard to the question how it could be assisted by an automated theorem prover. We will give further details of the proof methodology and present the proof obligations in a form that is amenable to automated deduction systems. 1 Introduction The investigations reported in this note were triggered by the discussions within the nationwide project Deduktion of the DFG on challenge problems that could be used to evaluate the various theorem provers, that have been used and developped within the project. One suggestion that received some attention was the formal verification of the correctness of a Prolog compiler described in [Borger and Rosenzweig 92]. In this paper the authors start from a formal specification of Prolog using the familiar computation tree model and arrive after successive refinement steps at a formal description of Prolog at the Warren abstract machine..