JVM Semantics and Tools
Defining reference semantics for Java bytecodes that takes into account concurrency.
- Java memory model
Comparing different JVM implementations using testing, and comparing them to reference semantics.
- how do we do testing in the presence of non-determinism (e.g. concurrency)
- Verified Java Bytecode Verification, by Gerwin Klein
- ACL2 Bytecode Proofs