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)

• JACK
  • http://www-sop.inria.fr/everest/personnel/Mariela.Pavlova/JavaVerifAppl.pdf
  • http://www-sop.inria.fr/everest/soft/Jack/jack.html
• BALI
  • http://isabelle.in.tum.de/bali/
  • Verified Java Bytecode Verification, by Gerwin Klein
• ACL2 Bytecode Proofs
  • http://www.cs.utexas.edu/~moore/publications/tphol.5-14-06.pdf
• Dynamic semantics of Java bytecode