The goals of the Verifix-project is the construction of correct compilers for
imperative and object-oriented programming languages and
commercially available processors. The code generated by correct 
compilers should be as efficient as code generated by usual unverified
compilers. This paper sketches how to prove the correctness of
transformations to intermediate code and memory-mappings performed by
compilers using abstract state machines.