History for Specification languages

added:
- *Refinement Verifier* The refinement verifier challenge
consists in enhancing current logical or computer-based verification
systems by means to prove the correctness of ASM refinement steps. A
concrete example of this challenge is the following challenge.
 
- *Java/JVM and C#/CLR Verification*  Verify by existing mechanical
theorem proving systems the following theorems, proved in the "*Jbook*
(2003)":http://www.inf.ethz.ch/~jbook using layered ASM models for
interpreters of Java and the 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 the 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":/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