Starting point: two “semi-formal” specifications
- Goldberg, Allen. “A Specification of the JVM Loading and Bytecode Verifier”. To appear in, Proceedings, 5th ACM Conference on Computer and Communications Security, San Francisco, October 1998. ftp://ftp.kestrel.edu/pub/papers/goldberg/Bytecode.pdf
- Qian, Zhenyu. “A Formal Specification of Java™ Virtual Machine Instructions for Objects, Methods and Subroutines”. To appear in, Jim Alves-Foss (Ed.), Formal Syntax and Semantics of Java(TM). Springer-Verlag LNCS, 1998. ftp://ftp.kestrel.edu/pub/papers/qian/abs-fsjvm.html