Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct.

Wolfgang Goerigk, Ulrich Hoffmann

Browse the full FM paper archive.