Thursday
========

9:00 -  9:30 Welcome
9:30 - 10:30 Einar Broch Johnsen (Creol: A Formal Model of Distributed 
                                  Concurrent Objects)

10:30 - 11:00 Coffee

11:00 - 11:30 Benjamin Weiß (Inferring Invariants by Static Analysis in KeY)
11:30 - 12:00 Marcus Baum (Debugging by Visualizing Symbolic Execution)
12:00 - 12:30 Christian Engel (Formal Verification of Performance Contracts)

12:45 - 13:45 Lunch

14:00 - 14:30 Philipp Ruemmer (Integer Arithmetic in KeY)
14:30 - 15:30 Discussion: Java 1.5 and Beyond  (Chair: Bernhard Beckert)
              14:30 - 15:00 Mattias Ulbrich (Verification of Java 5 Programs)
              15:00 - 15:30 Richard Bubel, Vladimir Klebanov (Implementing 
                                KeY in Java 5 - Pros and Cons)

15:30 - 16:00 Coffee

16:00 - 16:15 Daniel Larsson (Automatic Failure Case Generation)
16:15 - 16:30 Helga Velroyen (Non-termination Proofs in Dynamic Logic)
16:30 - 17:00 Christoph Gladisch (White-box Testing)
17:00 - 18:00 New Features Session
	      Markus Bender (White-box Testing)
	      Volker Klasen, Joachim Pehl (New Proof Navigation)
	      Denis Lohner (New JML Translation) 
	      ...


Friday
======

 9:00 - 10:00 Frank Piessens (Concern-specific Specification and Verification 
                              to Improve Software Quality and Security)
10:00 - 10:30 Vladimir Klebanov (Verifying Library Code for Concurrent Access)

10:30 - 11:00 Coffee

11:00 - 11:30 Richard Bubel (Verification of the Schorr-Waite Algorithm)
11:30 - 12:00 Peter H. Schmitt (The Mondex Case Study)
12:00 - 12:15 Frank Werner (Analysing Probabilistic Network Flooding)
12:15 - 12:45 Denis Lohner (Specifying the Java Collections Framework in JavaDL)

12:45 - 13:45 Lunch

14:00 - 14:30 Gerd Beuster (The Verisoft Email Client)
14:30 - 14:45 Reiner Hähnle (Agile Formal Methods)
14:45 - 15:30 Discussion: Teaching Formal Methods (Chair: Reiner Hähnle)

15:30 - 16:00 Coffee

16:00 - 16:30 Thorsten Bormer (Multi-formalism Specification and
                               Verification in Verisoft)
16:30 - 16:45 Henrik Johansson (Linear Unification Constraints vs 
                                ACU-Unification)
16:45 - 17:15 Oleg Mürk (Deductive Verification of C Programs with KeY)
17:15 - 18:00 Discussion: Non-determinism in Programs (Chair: Wolfgang Ahrendt)
              Vladimir Klebanov: Concurrency and Non-determinism
              Oleg Muerk: Non-determinism in C
              Further topics: Non-determinism vs. Underspecification, t=t?

Saturday
========

 9:00 - 10:00 Joe Kiniry (Recent Advances in Extended Static Checking)
10:00 - 10:30 Wojciech Mostowski (Fully Verified Java Card API Reference 
                                  Implementation)

10:30 - 11:00 Coffee

11:00 - 11:30 André Platzer (Differential Dynamic Logic for Hybrid Systems) 
11:30 - 11:55 Bernhard Beckert (Proving the Soundness of KeY)
11:55 - 12:00 Closing Session

??? Lunch