Proving WAM compiler correctness
Peter H. Schmitt · 1994
In this note we analyse the proof of compiler correctness of the WAM given in the paper The WAM - Definition and Compiler Correctness by Egon Boerger and Dean Rosenzweig. TR-14/92, Dipartimento di Informatica, Universita di Pisa, 1992. 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.