Sciweavers

Share
CADE
2002
Springer

Formal Verification of a Java Compiler in Isabelle

13 years 5 days ago
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.
Martin Strecker
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2002
Where CADE
Authors Martin Strecker
Comments (0)
books