4th KeY Symposium 2005

Wednesday (June 8th, 2005)

  08.30 Bus departures from Chalmers
  08.40 Bus departures from Nice Hotel
  09.30 Arrival at Lökeberg
  09.50 Coffee break
  10.15 Session (80min): New features                   [Reiner Hähnle]
     10.15 Christian Engel: The JML interface to KeY (30)
     10.45 Marius Hillenbrand: Eclipse plugin for the JML interface to KeY (15)
     11.00 Wojciech Mostowski: New .key Syntax (20)
     11.25 Benjamin Weiss: Renaming of program variables (Demo) (15)
  11.35 Lunch break (lunch served at 12.20)
  13.00 Session (75min): New features                   [Bernhard Beckert]
     13.00 Daniel Larsson: OCL Simplification (15)
     13.15 Hajo Daniels: Demo of the "new" GF editor for OCL (15)
     13.30 Marcus Baum: Visualisation of open goals in program proofs (30)
     14.00 Philipp Ruemmer: Quantified updates (15)
  14.15 Break
  14.35 Session (60min): Invited talks                  [Peter Schmitt]
     14.35 Martin Giese: Verified Provers (30)
     15.05 Andre Platzer: Abstraction Refinement for Hybrid Systems (30)
  15.35 Coffee break
  15.55 Session (60min): Invited talk + Concurrency     [Martin Giese]
     15.55 Elmar Habermalz: KeY at sd&m - a vision and a lot of work (30)
     16.25 Vladimir Klebanov: Towards Deductive Verification of Concurrent Java Software (30)
  16.55 Break
  17.10 We meet outside the conference center
  17.30 Boat ride
  20.00 Dinner is served

Thursday (June 9th, 2005)

  07.30 Breakfast
  08.30 Session (90min): OCL, Specifications
     08.30 Kristofer Johannisson: Translating OCL to Natural Language (30)
     09.00 Rogardt Heldal: Relating Formal and Informal Contracts using Domain Models (30)
     09.30 Slavisa  Markovic: Refactoring of UML Diagrams annotated with OCL (30)
  10.00 Coffee break
  10.30 Session (50min): Invited Talk + Proving Techniques
     10.30 Erik Poll: Immutable Objects (30)
     11.00 Richard Bubel: ADT techniques for KeY (20)
  11.20 Break
  11.30 Session (45min): Analysing Java + Loops
     11.30 Philipp Ruemmer: Generating counterexamples for program correctness (15)
     11.45 Steffen Schlager: An Invariant Rule for Dynamic Logic Using Change Information (30)
  12.15 Lunch break (lunch served at 12.20)
  13.45 Session (90min): Loops
     13.45 Angela Wallenburg: Customised Induction Rules (30)
     14.15 Thomas Baar: Proving loops with KeY -- An Experience Report (30)
     14.45 Tobias Gedell:  Loop Analysis in KeY (30)
  15.15 Coffee break
  15.45 Session (80min): Dynamic Logic and Calculi
     15.45 Roger Antonsen: Uniform Variable Splitting (20)
     16.05 Andreas Roth: The proof obligations of KeY (30)
     16.35 Holger Stenger: Classification of Taclets (15)
     16.50 Thorsten Bormer: Managing a changing rule base (15)
  17.05 Break
  18.15 Dinner is served

Friday (June 10th, 2005)

  07.30 Breakfast
  08.30 Session (65min): C(0) Verification
     08.30 Markus Wagner: Proving C0 programs correct with Isabelle (15)
     08.45 Christoph Gladisch: A C0 proof system with KeY (30)
     09.15 Daniel Larsson: Making KeY ready for C verification (20)
  09.35 Coffee break
  10.05 Session (75min): Verisoft + Information Flow
     10.05 Niklas Henrich: The Verisoft Email Client case study (15)
     10.20 Gerd Beuster: Formalizing Security Properties of User Interfaces (30)
     10.50 Jing Pan: Information Flow Analysis with KeY (30)
  11.20 Lunch Break + Check out (lunch served at 12.00)
  13.00 Discussion: ?
  14.15 Coffee break
  14.45 Discussion: ?
  15.45 Break
  16.00 Discussion: ?
  17.00 Break
  17.15 Bus back