3rd KeY Symposium 2004

Invited Talks

1. Maria Paola Bonacina - Experiments and open issues on decision procedures, theorem proving and software analysis
2. Mads Dam - First-Order Mu-Calculus as a Framework for Program Verification
3. Werner Stephan - Verification of Imperative Programs

Karlsruhe

1. Richard Bubel - Verifying with ShapeGraphs and SchorrWaite
2. Hans-Joachim Daniels
3. Christian Engel - Translation from JML to DL
4. Wolfram Menzel
5. André Platzer - A Calculus for an Object-Oriented Dynamic Logic with Updates
6. Andreas Roth - Modular Verification
7. Philipp Ruemmer - CSP and Verification of JCSP programs / correctness of taclets
8. Ignaz Rutter - Agilent/GeneralStore
9. Ralf Sasse - Modifies clauses, their verification and use
10. Steffen Schlager - Verification of concurrent systems
11. Peter Schmitt
12. Holger Stenger - Strategies in the KeY Prover

Goeteborg

1. Wolfgang Ahrendt - An OCL Case Study
2. Tobias Gedell - Future research and demo of a program analysis implemented in KeY
3. Martin Giese - From use cases to post conditions
4. Reiner Haehnle
5. Kristofer Johannisson - OCL parsing/type checking and GF
6. Daniel Larsson - Partial Evaluation of OCL
7. Wojciech Mostowski - Verification of Safety Properties in the Presence of Transactions
8. Aarne Ranta (with contribution from Hajo and Kristofer) - Informal and formal specifications: the next phase
9. Rogardt Heldal

Koblenz

1. Bernhard Beckert
2. Pia Breuer
3. Gerd Beuster - Verisoft Email Client
4. Jonas Gerdel
5. Christoph Gladisch
6. Vladimir Klebanov - Java Concurrency and Proof Reuse
7. Markus Maron
8. Nicolaus Spies
9. Annekatrin Tretow

Lausanne

1. Thomas Baar - Fondue Toolset
2. Frédéric Fondement - Towards an MDA-Oriented UML Profile for Distribution
3. Slavisa Markovic - Composition of OCL-Described Rafactoring Rules

Zuerich

1. Stanislas Nanchen - ASMKeY

Clausthal

1. Frank Stamm - The VTool Project