3rd KeY Symposium 2004
Sunday (June 6th, 2004)
Arrival
18:00
Dinner
Monday (June 7th, 2004)
7:30am - 8:30am
Breakfast
8:30am - 10:30am
- Welcome
- Invited Talk: Maria Paola Bonacina - Experiments and open issues on decision procedures, theorem proving and software analysis
- Wojciech Mostowski - Verification of Safety Properties in the Presence of Transactions
- Vladimir Klebanov - Java Concurrency (short)
10:30am - 11:00am
Coffee Break
11:00am - 12:30pm
- Daniel Larsson - Partial Evaluation of OCL
- Steffen Schlager - A Temporal Logic for Programs (short)
- Philipp Ruemmer - Correctness of taclets (short)
- André Platzer - A Calculus for an Object-Oriented Dynamic Logic with Updates (short)
12:45pm - 14:00pm
Lunch
14:00pm - 15:30pm
- Invited Talk: Werner Stephan - Verification of Imperative Programs
- Frank Stamm - The VTool Project
15:30pm - 16:00pm
Coffee Break
16:00pm - 18:00pm
- Vladimir Klebanov, Andreas Roth - Overview and Demo of new KeY features
- Andreas Roth - Modular Verification
- Martin Giese - From informal to formal specification
- Christian Engel - Translation JML->DL (short)
- Wolfgang Ahrendt - An OCL case study (very short)
19:00pm
Barbecue at Onkel Hakki's
Tuesday (June 8th, 2004)
7:30am - 8:30am
Breakfast
8:30am - 10:30pm
- Invited Talk: Mads Dam - First-Order Mu-Calculus as a Framework for Program Verification
- Philipp Ruemmer - CSP and Verification of JCSP Programs
- Gerd Beuster - The Verisoft Project and the Verisoft Email Client
10:30am - 11:00am
Coffee Break
11:00am - 12:40pm
- Stanislas Nanchen - ASMKeY
- Tobias Gedell - Future research and demo of a program analysis implemented in KeY
- Frédéric Fondement - Towards an MDA-oriented UML Profile for distribution (short)
- Slavisa Markovic - Composition of OCL-described refactoring rules (short)
12:45pm - 14:00pm
Lunch
14:00pm - 15:30pm
- Holger Stenger - Strategies in the KeY Prover (short)
- Ignaz Rutter - Agilent/GeneralStore (short)
- Ralf Sasse - Modifies clauses, their verification and use (short)
- Thomas Baar - Fondue Toolset
15:30pm - 16:00pm
Coffee Break
16:00pm - 18:00pm
- Vladimir Klebanov - Proof Reuse
- Richard Bubel - Verifying with ShapeGraphs and SchorrWaite
- Arne Ranta (with contribution from Hajo and Kristofer) - Informal and formal specifications: the next phase
- Kristofer Johannisson - OCL parsing/type checking and GF
18:15pm
Dinner
Wednesday (June 9th, 2004)
8:00am - 9:00am
Breakfast
9:00am - 10:30am
Discussion 1: The Future
10:30am - 11:00am
Coffee Break
11:00am - 12:30am
Discussion 2: Infrastructure, Tools, Languages
12:45pm - 14:00pm
Lunch
14:00am - 15:30am
Discussion 3: Proof Procedure, Calculus, Rules
15:30pm - 18:00pm
Excursion to Castle Drachenburg