Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

11

CADE
2002
Springer

favoriteEmaildiscussreport

147views Logical Reasoning» more CADE 2002»

Formal Verification of a Java Compiler in Isabelle

14 years 5 months ago

Formal Verification of a Java Compiler in Isabelle

Download www.irit.fr

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

Real-time Traffic

Automated Reasoning | CADE 2002 | Compiler Correctness Proof | Formal Proof | Proof Environment Isabelle |

claim paper

Related Content

» Verifying CPS transformations in IsabelleHOL

» Verifying the CPS Transformation in IsabelleHOL

» Verifying a Compiler for Java Threads

» Pervasive Compiler Verification From Verified Programs to Verified Systems

» Verification of Java Programs with Generics

» A Certified Implementation on Top of the Java Virtual Machine

» Ott effective tool support for the working semanticist

» Optimisation Validation

» Java Implementation Verification Using Reverse Engineering

Post Info
More Details (n/a)

Added	03 Dec 2009
Updated	03 Dec 2009
Type	Conference
Year	2002
Where	CADE
Authors	Martin Strecker

Comments (0)