Formal Verification of a Java Compiler in Isabelle

This paper reports on the formal proof of correctness of a compiler from 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.
 

Online Copy

Available as PDF

This paper is published in the Springer LNCS series. © Springer-Verlag.
 
 

Isabelle Sources

Available as gzip tar, awaiting integration into the Isabelle distribution...
 

BibTeX Entry

@InProceedings{strecker02:verif_java_compil,
  author = 	 {Martin Strecker},
  title = 	 {Formal Verification of a {Java} Compiler in {Isabelle}},
  booktitle = 	 {Proc. Conference on Automated Deduction (CADE)},
  year =	 2002,
  volume =	 2392,
  series =	 {Lecture Notes in Computer Science},
  publisher =	 {Springer Verlag},
  pages=         {63--77}
}