4th KeY Symposium 2005

Pictures & Slides

Roger Antonsen		Uniform Variable Splitting
Thomas Baar		How to Prove Loops to be Correct?
Marcus Baum		Visualisation of Open Goals in KeY
Gerd Beuster		Formalizing Security Properties of User Interfaces
Thorsten Bormer		Managing a changing rule base
Richard Bubel		Can we make use of ADTs in KeY?
Hajo Daniels		Demo of the "new" GF editor for OCL
Christian Engel		JML Model Fields
Tobias Gedell		Loop Analysis in KeY
Martin Giese		Verified Provers
Christoph Gladisch		Towards the verification of C with KeY
Elmar Habermalz		KeY at sd&m - a vision and a lot of work
Rogardt Heldal		Relating Formal and Informal Contracts using Domain Models
Niklas Henrich		The Verisoft Email Client case study
Marius Hillenbrand		Eclipse plugin for the JML interface to KeY
James Hunt		KeY + Hija
Kristofer Johannisson		Translating OCL to Natural Language
Vladimir Klebanov		Towards Deductive Verification of Concurrent Java Software
Daniel Larsson		Design Pattern Mechanism with OCL
Daniel Larsson		KeY Version for MISRA C
Slavisa Markovic		Refactoring of UML Diagrams annotated with OCL
Wojciech Mostowski		New .key Syntax
Jing Pan		Secure Information Flow Analysis using KeY
Andre Platzer		Abstraction Refinement for Hybrid Systems
Erik Poll		/@ immutable @/ objects
Andreas Roth		KeY Proof Obligations
Philipp Ruemmer		Quantified Updates
Philipp Ruemmer		Generating Counterexamples for Java Dynamic Logic
Steffen Schlager		An Improved Rule for While Loops in Deductive Program Verification
Holger Stenger		Classification of Taclets
Markus Wagner		Proving C0 programs correct with Isabelle
Angela Wallenburg		Customised Induction Rules for Proving Correctness of Imperative Programs
Benjamin Weiss		Demo: (Re)naming of program variables

More Pictures

Album of Wojciech Mostowski

Album of Gerd Beuster