Java and the Java Virtual Machine

Definition, Verification, Validation

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

Table of contents

  1. Front Matter
    Pages I-X
  2. Introduction

    1. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 1-13
  3. Abstract State Machine

    1. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 15-28
  4. Java

    1. Front Matter
      Pages 29-32
    2. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 33-46
    3. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 47-69
    4. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 71-85
    5. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 87-94
    6. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 95-110
    7. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 111-134
  5. Compilation of Java: The Trustful JVM

    1. Front Matter
      Pages 135-137
    2. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 139-146
    3. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 147-154
    4. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 155-158
    5. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 159-164
    6. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 165-166
    7. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 167-203
  6. Bytecode Verification: The Secure JVM

    1. Front Matter
      Pages 205-207
    2. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 209-222
    3. Robert F. Stärk, Joachim Schmid, Egon Börger
      Pages 223-271

About this book

Introduction

This book provides 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  which can be used for testing code. The method developed for this purpose is based on Abstract State Machines (ASMs) and can be applied to other virtual machines and to other programming languages as well. The book is written for advanced students and for professionals and practitioners in research and development who need for their work a complete and transparent definition and an executable model of the language and of the virtual machine underlying its intended implementation.

Keywords

C programming language Constraint Java Java Card Java Virtual Machine Natural programming programming language security testing validation virtual machine

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

Bibliographic information

  • DOI https://doi.org/10.1007/978-3-642-59495-3
  • Copyright Information Springer-Verlag Berlin Heidelberg 2001
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Springer Book Archive
  • Print ISBN 978-3-642-63997-5
  • Online ISBN 978-3-642-59495-3
  • About this book
Industry Sectors
Electronics
Telecommunications
Aerospace