Jbook

Citation:	Robert Stärk, Joachim Schmid, and Egon Börger, Java and the Java Virtual Machine: Definition, Verification, Validation. Springer-Verlag, 2001.
Summary:	A high-level description, together with a mathematical and an experimental analysis, of Java and of the Java Virtual Machine (JVM), including a standard compiler of Java programs to JVM code and the security critical bytecode verifier component of the JVM. The description is structured into language layers and machine components. It comes with a natural executable refinement (written in AsmGofer and provided on CD-ROM) which can be used for testing code.
Subjects:	Java, Compiler Correctness, Verification, ASM Books
Download:	May be purchased from Springer-Verlag. Additional material (slides, table of contents, errata, etc.) can be found at the Jbook website at http://www.inf.ethz.ch/~jbook/.
Notes:	"The Jbook gives the most comprehensive and consistent formal account of the combination of Java and the JVM." (Pieter Hartel and Luc Moreau in ACM Computing Surveys 2001, "Formalizing the Safety of Java, the Java Virtual Machine and Java Card" , Section 6.2).

Abstract State Machines