We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pe...
This paper reports on the formal proof of correctness of a compiler from a substantial subset of Java source language to Java bytecode in the proof environment Isabelle. This work ...