4th KeY Symposium 2005

Karlsruhe

1. Peter Schmitt -
2. Steffen Schlager - An Invariant Rule for Dynamic Logic Using Change Information
3. Richard Bubel - ADT techniques for KeY
4. Andreas Roth - The proof obligations of KeY
5. Holger Stenger - Classification of Taclets
6. Marius Hillenbrand - Eclipse plugin for the JML interface to KeY
7. Benjamin Weiss - Renamings of Program Variables
8. Christian Engel - The JML interface to KeY
9. Marcus Baum - Visualisation of open goals in program proofs
10. Isabell Tonin -

Gothenburg

1. Reiner Hähnle -
2. Wolfgang Ahrendt -
3. Philipp Rümmer - Generating counterexamples for program correctness
4. Tobias Gedell - Loop Analysis in KeY
5. Kristofer Johannisson - Translating OCL to Natural Language
6. Angela Wallenburg - Customised Induction Rules
7. Hans-Joachim Daniels - Demo of the "new" GF editor for GF
8. Daniel Larsson - OCL Simplification
9. Wojciech Mostowski - New .ket Syntax
10. Jing Pan - Information Flow Analysis with KeY
11. Muhammad Ali Shah -
12. Xavier Leblanc -

Koblenz

1. Bernhard Beckert -
2. Gerd Beuster - Formalizing Security Properties of User Interfaces
3. Vladimir Klebanov - Towards Deducive Verification of Concurrent Java Software
4. Niklas Henrich - The Verisoft Email Client case study
5. Markus Wagner - Proving C0 programs correct with Isabelle
6. Cristoph Gladisch - A C0 proof system with KeY
7. Thorsten Bormer - Managing a changing rule base

External

1. Dennis Walter -
2. Martin Giese - Verified Provers
3. Thomas Baar - Proving loops with KeY -- An Experience Report
4. Slavisa Markovic - Refactoring of UML Diagrams annotated with OCL
5. Elmar Habermalz - KeY at sd&m - a vision and a lot of work
6. Erik Poll - Immutable Objects
7. Roger Antonsen - Uniform Variable Splitting
8. Christian Mahesh Hansen -
9. Andre Platzer - Abstraction Refinement for Hybrid Systems