Abstract |
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} }
Last modified: Sat Nov 11 20:36:57 CET 2006 |