History for JBook Milestone

added:
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":/http://www.inf.ethz.ch/personal/fruja/,http://www.di.unipi.it/~boerger.
A similar project, mechanically verifying "a mathematical
proof":http://www.di.unipi.it/~boerger/prologwam.html for the
correctness of a compilation scheme from Prolog programs to Warren
Abstract Machine (WAM) code starting from an ASM for "*ISO
Prolog*":ftp://ftp.di.unipi.it/pub/Papers/boerger/prolog.ps and
leading through 12 ASM refinement steps to an ASM for the
"*WAM*":ftp://ftp.di.unipi.it/pub/Papers/boerger/wam.ps, has been
successfully carried out in the 1990'ies using the "KIV
prover":http://www.eecs.umich.edu/gasm/papers/wamcase.html