Milestone for compiler verification

Verify by existing mechanical theorem proving systems the following theorems proved in the Jbook for abstract interpreters of Java and the JVM defined there. Refine the models to the current version of Java/JVM and use the theorem prover to extend the proofs to the extended models of Java/JVM.

• 1. Java is type safe (Thm.8.4.1)
• 2. Correctness of the Java2JVM compilation scheme (Thm.14.1.1
• 3. JVM Invariants for soundness of Bytecode Type Assignments (Thm.16.4.1)
• 4. Completeness of the scheme for certifying Java2JVM compilation (Thm.16.5.1,16.5.2)
• 5. Soundness of the bytecode verifier (Thm.17.1.1)

Part of this challenge consists in providing modular proof schemes that reflect the hierarchy of the layered ASM models for Java/JVM. Reuse the computer-based verification of the JavaCard-without-subroutines subset of Java (see Gerwin Klein and Tobias Nipkow, A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler, TR 0400001T.1, National ICT Australia, 2004 and to appear in ACM TOPLAS and G. Betarte, E. Gimenez, C. Loiseaux, B. Chetali. FORMAVIE: Formal Modelling and Verification of the Java Card 2.1.1 Security Architecture. Proc. eSmart 2002). Reuse the Java/JVM verification proofs to establish the corresponding theorems for C#/.NET CLR, using the corresponding ASM models developed in a series of recent papers. A similar project, mechanically verifying a mathematical proof for the correctness of a compilation scheme from Prolog programs to Warren Abstract Machine (WAM) code starting from an ASM for ISO Prolog and leading through 12 ASM refinement steps to an ASM for the WAM, has been successfully carried out in the 1990'ies using the KIV prover