KeY-Symposium 2006 - Final Program

Tuesday, 6-th June

Time	Topic	Category
9.00 - 9.30	Welcome	Who is Who?
9.30 - 9.45	D. Lohner: The New OCL to DL Translation	New Features
9.45 - 10.05	B. Weiss : The New Proofobligations
10.05 - 10.20	M. Schroeder: DFA Annotations
10.20 - 10.35	M. Baum: Proof Visualization
10.35 - 11.00	Pause
11.00 - 11.30	V. Klebanov: A Dynamic Logic for Deductive Verification of Concurrent programs	Concurrency
11.30 - 11.50	J. Pehl: See the rules unfold
11.50-12.10	T. Oliwa: Understand the Java Memory Model
12.10 - 12.25	A. Kuwertz: SMT Library Support	Automation
12.30 - 14.00	Lunch
14.00 - 14.15	P. Rümmer: Constraints modulo Presburger Arithmetic	Automation (Cnt'd)
14.15 - 15.00	Discussion: Proof Automation (Moderator: P. Rümmer)
15.00 - 15.30	Pause
15.30 - 15.50	T. Bormer: Proof Reuse when Verification Systems are Modified	Automation (Cnt'd)
15.50 - 16.20	T. Gedell: Loop Parallelization: demo and planned new work	Loops
16.20 - 16.40	M. Krebs: Support of Loop Proofs in KeY with BLAST
16.40 - 17.00	Pause
17.00 - 17.20	M. Wagner Error Modelling	Verisoft
17.20 - 17.50	G. Beuster: Formalizing GOMS models

In the evening we will have a sightseeing tour through the town of Speyer (starting at 19.15).

Time	Topic	Category
9.00 - 9.45	Peter Müller - Reasoning about Method Calls in Interface Specifications	Invited Talk
9.45 - 10.15	W. Mostowski: Formalization of non-atomic JavaCard Methods in KeY	Formalization and Specification
10.15 - 10.35	S. Markovic: Refactoring OCL
10.35 - 11.00	Pause
11.00 - 11.30	P. Rümmer: Formalization of Quantified Updates in Isabelle	Theory
11.30 - 12.00	S. Schlager: Global Discharge - A Unified Rule for Loop Verification
12.00 - 12.30	D. Walter : Type Based Deduction
12.30 - 14.00	Lunch
14.00 - 14.45	Arnd Poetzsch-Heffter - Modular Specification of Encapsulated Object-Oriented Components	Invited Talk
14.45 - 15.15	Modelling System Invariants (B.Beckert, S. Schlager and R. Bubel) (part1, part2)	Theory (Ctn'd)
15.15 - 15.45	Pause
15.45 - 16.15	C. Wonnemann: Formal Specification of Avionic software	Case Study, Killer Application
16.15 - 16.45	Discussion: Killer Application for KeY (Moderator: R. Hähnle)
16.45 - 17.00	Pause
17.00 - 17.30	D. Larsson: Symbolic Fault Injection	Applications
17.30 - 17.45	L.T. Klauwer: Evaluation of Symbolic Fault Injection

Time	Topic	Category
9.00 - 9.30	C. Engel: Verification Based Test Case Generation	Applications (Ctn'd)
9.30 - 10.00	C. Gladisch: Verification of C programs with KeY	C0, MisraC
10.00 - 10.15	S. Kekkonen: Extending KeY to handle C programs
10.15 - 10.45	Pause
10.45 - 11.45	Discussion: KeY Book (Moderator: P.H. Schmitt)	The Road To Verified Software