9th KeY Symposium 2010 -- Programme
Last modification: 25/05/2010, 10:14
Jump to: Tuesday, Wednesday, Thursday
Tuesday, 25th May
Time |
Topic |
| 10:00 -- 10:30 | Welcome coffee |
| 10:30 -- 10:40 | Opening of the 9th Annual KeY Symposium |
| 10:40 -- 11:10 | Dynamic Frames in JML Benjamin Weiß [slides] |
| 11:10 -- 11:40 | Combining Formal and Agile Methods David Faragó [slides] |
| 11:40 -- 12:00 | Verification Based Test Case Generation for Scoped Memory in Safety-Critical Java Gabriele Paganelli [slides] |
| 12:00 -- 12:30 | Test-Based Inference of Polynomial Loop-Bound Functions Rody Kersten [slides] |
| 12:30 -- 14:00 | Lunch break |
| 14:00 -- 15:00 | Automated Termination Analysis of Java Bytecode by Term Rewriting
(Invited Talk) Jürgen Giesl (RWTH Aachen, Germany) |
| 15:00 -- 15:45 | Design of the HATS Core ABS (Abstract Behavioral Specification) Language Reiner Hähnle [slides] |
| 15:45 -- 16:15 | Coffee break |
| 16:15 -- 16:45 | A Dynamic Logic for Unstructured Programs Mattias Ulbrich |
| 16:45 -- 17:15 | Model Generation for Quantified First-order Logic Formulas Christoph Gladisch [slides] |
| 17:15 -- 17:30 | New Features Session: Overview of KeY 1.6 Richard Bubel [slides] |
| 17:30 -- 17:45 | New Features Session: Using Taclets for the SMT
Integration of KeY Benjamin Niedermann |
| 17:45 -- 18:15 | Discussion:
Progress Report Moderation: Peter H. Schmitt |
Wednesday, 26th May
Time |
Topic |
| 09:00 -- 10:00 | Attribute Grammars for the Specification of Histories in JML
(Invited Talk) Frank de Boer (Leiden University, The Netherlands) |
| 10:00 -- 10:40 | Compositional Semantics and Verification of Asynchronous Objects Wolfgang Ahrendt |
| 10:40 -- 11:10 | Coffee break |
| 11:10 -- 11:30 | CML, a Modelling Language for Creol Giampiero Baggiani |
| 11:30 -- 11:50 | Implementing Partial Evaluator via Symbolic Execution Ran Ji [slides] |
| 11:50 -- 12:10 | Towards a Proof Management for KeY Daniel Bruns [slides] |
| 12:10 -- 12:40 | Discussion:
The Role of KeY Within COST Action IC0701 Moderation: Bernhard Beckert |
| 12:40 -- 14:00 | Lunch break |
| 14:00 -- 14:30 | Delta-oriented Development of Software Product Lines Ina Schaefer [slides] |
| 14:30 -- 14:50 | Verification of Software Product Lines Vladimir Klebanov and Ina Schaefer [slides] |
| 14:50 -- 15:20 | Mind the Gap: Formal Verification and the Common Criteria Sarah Grebing and Bernhard Beckert |
| 15:50 | Bus transfer to Baden-Baden (from Gernsbach Bahnhof) |
| 16:30 -- 18:00 | Guided Tour at Museum Frieder Burda in Baden-Baden |
| 19:00 | Dinner at Sonnenhof in Gernsbach (bus departs 18:03 or 18:33 from Baden-Baden) |
Thursday, 27th May
Time |
Topic |
| 09:00 -- 09:30 | Program Annotations for Verifying Compilers: Theory vs. Practice Bernhard Beckert |
| 09:30 -- 10:00 | Formal Verification of Rewrite Rules for Compiler Backends David Dueck |
| 10:00 -- 10:30 | The Low-Level Bounded Model Checker (LLBMC) Stephan Falke [slides] |
| 10:30 -- 11:00 | Coffee break, Group Photograph |
| 11:00 -- 11:30 | Closures in Java Gregor Bethlen [slides] |
| 11:30 -- 12:30 | Discussion: Challenges to Verification,
Future of the KeY Project Moderation: Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt |
| 12:30 -- 14:00 | Lunch, Departure |