article · 1998
A Specification of Java Loading and Bytecode Verification
Allen Goldberg Kestrel, Allen Goldberg
Cited by 0Abstract and details only
Abstract
This paper gives a mathematical specification the Java Virtual Machine (JVM) bytecode verifier. The specification is an axiomatic description of the verifier that makes precise subtle aspects of the JVM semantics and the verifier. We focus on the use of data flow analysis to verify type-correctness and the use of typing contexts to insure global type consistency in the context of an arbitrary strategy for dynamic class loading. The specification types interfaces with sufficient accuracy to eliminate run-time type checks. Our approach is to specify a generic dataflow architecture and formalize the JVM verifier as an instance of this architecture. The emphasis in this paper is on readability of the specification and mathematical clarity. The specification given is consistent with the descriptions in the Lindholm's and Yellin's The Java^TM Virtual Machine Specification. It less committed to certain implementation choices than Sun's version 1.1 implementation. In particular, the specification does not commit an implementation to any loading strategy, and detects all type errors as early as possible.
Cite this paper
Kestrel, A. G., & Goldberg, A. (1998). A Specification of Java Loading and Bytecode Verification.
Kestrel, Allen Goldberg, and Allen Goldberg. “A Specification of Java Loading and Bytecode Verification.” 1998.
Kestrel, Allen Goldberg, and Allen Goldberg. 1998. “A Specification of Java Loading and Bytecode Verification.”
Kestrel, A.G. and Goldberg, A. (1998) ‘A Specification of Java Loading and Bytecode Verification’.
@article{kestrel1998specification,
title = {{A Specification of Java Loading and Bytecode Verification}},
author = {Kestrel, Allen Goldberg and Goldberg, Allen},
year = {1998}
}Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.