A formal framework for the Java bytecode language and verifier
- 1 October 1999
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 34 (10) , 147-166
- https://doi.org/10.1145/320384.320397
Abstract
This paper presents a sound type system for a large subset of the Java bytecode language including classes, interfaces, constructors, methods, exceptions, and bytecode subroutines. This work serves as the foundation for developing a formal specification of the bytecode language and the Java Virtual Machine's bytecode verifier. We also describe a prototype implementation of a type checker for our system and discuss some of the other applications of this work. For example, we show how to extend our work to examine other program properties, such as the correct use of object locks.Keywords
This publication has 13 references indexed in Scilit:
- A simple, comprehensive type system for Java bytecode subroutinesPublished by Association for Computing Machinery (ACM) ,1999
- A compositional account of the Java virtual machinePublished by Association for Computing Machinery (ACM) ,1999
- JResPublished by Association for Computing Machinery (ACM) ,1998
- From system F to typed assembly languagePublished by Association for Computing Machinery (ACM) ,1998
- A type system for Java bytecode subroutinesPublished by Association for Computing Machinery (ACM) ,1998
- Javalight is type-safe---definitelyPublished by Association for Computing Machinery (ACM) ,1998
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- Java is type safe — ProbablyPublished by Springer Nature ,1997
- TILACM SIGPLAN Notices, 1996
- A Proposal for Making Eiffel Type-safeThe Computer Journal, 1989