8.30    Invited talk:    Understanding Java: from languages towards systems     Martin Abadi
9.05    Formal Underpinnings of Java: Some requirements     Rich Cohen

9.15    The Costs and Benefits of Java Bytecode Subroutines   Stephen Freund
9.40    The Functions of Java Bytecode    Mark Jones

10.05    Coffee

10.35   Type-based Assessment of the Java Byte-level Language    Anthony Smith
11.00    Java Bytecode Verification using Model Checking   Harald Vogt
11.25    Toward a Provably-Correct Implementation of the JVM Bytecode Verifier   Alessandro Coglio

12.00    Lunch

1.30    Invited talk:    Sun's angle     Gilad Bracha
1.45    Lightweight Bytecode Verification    Eva Rose
2.05    Proving the Soundness of a Java Bytecode Verifier in Isabelle/HOL   Cornelia Pusch

2.35    Coffee

3.00    JML: a Java Modeling Language    Gary Leavens
3.25    A proposal for an abstract semantics of shared objects in multi-threaded Java    Gianna Reggio
4.50    Formal Executable Semantics for Java    Marjorie Russo
4.15    Safe and Verifiable Design of Multithreaded Java Programs with CSP and FDR    Dyke Stiles

4.20    Wrapping up