Formal Verification of a Java Compiler in Isabelle

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 is based on extensive previous formalizations of Java, which comprise all relevant features of object-orientation. We place particular emphasis on describing the effects of design decisions in these formalizations on the compiler correctness proof.

• Type: Conference
• Year: 2002
• Where: CADE
• Authors: Martin Strecker
• Keywords: Automated Reasoning, CADE 2002, Compiler Correctness Proof, Formal Proof, Proof Environment Isabelle