• Robert F. Stärk
  • Joachim Schmid
  • Egon Börger


This book provides a structured and high-level description, together with a mathematical and an experimental analysis, of Java and of the Java Virtual Machine (JVM), including the standard compilation of Java programs to JVM code and the security critical bytecode verifier component of the JVM. The description is structured into modules (language layers and machine components), and its abstract character implies that it is truly platform-independent. It comes with a natural refinement to executable machines on which code can be tested, exploiting in particular the potential of model-based high-level testing. The analysis brings to light in what sense, and under which conditions, legal Java programs can be guaranteed to be correctly compiled, to successfully pass the bytecode verifier, and to be executed on the JVM correctly, i.e., faithfully reflecting the Java semantics and without violating any run-time checks. The method we develop for this purpose, using Abstract State Machines which one may view as code written in an abstract programming language, can be applied to other virtual machines and to other programming languages as well.


Virtual Machine Java Program Java Virtual Machine Abstract State Machine Abstract Syntax Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Robert F. Stärk
    • 1
  • Joachim Schmid
    • 2
  • Egon Börger
    • 3
  1. 1.Theoretische InformatikETH ZentrumZürichSwitzerland
  2. 2.Siemens AGMünchenGermany
  3. 3.Dipartimento di InformaticaUniversità di PisaPisaItaly

Personalised recommendations