Sciweavers

CADE
2002
Springer
14 years 4 months 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 ...
Martin Strecker