Jump to: Monday, Tuesday, Wednesday
Time |
Topic |
| 09:15 -- 09:30 | Registration |
| 09:30 -- 09:40 | Wolfgang Ahrendt Opening of the 14th Annual KeY Symposium |
| 09:40 -- 10:00 | Peter Schmitt A short remark in a rather long story |
| 10:00 -- 10:30 | Richard Bubel Verification of TimSort |
| 10:30 -- 11:00 | Coffee break |
| 11:00 -- 12:00 | Invited talk: Matt Kaufmann ACL2 Support for Automated and Interactive Proof |
| 12:00 -- 13:30 | Lunch break |
| 13:30 -- 14:00 | Nathan Wasser Automatically Generating Specifications |
| 14:00 -- 14:30 | Simon Robillard Out of the Loop? How Vampire Can Help KeY Verify While-Loops |
| 14:30 -- 15:00 | Dominic Scheurer From Trees to DAGs: A General Lattice Model for Symbolic Execution |
| 15:00 -- 15:30 | Coffee break |
| 15:30 -- 16:00 | Mihai Herda
Using Formal Verification Techniques for Reliability Estimation |
| 16:00 -- 17:00 | New Features |
| 19:00 | Dinner at the Tapas Restaurant La Sombrita, Linnegatan 23, reachable by walk or by tram 1, from Brunnsparken, direction Tynnered, exit at Prinsgatan |
Time |
Topic |
| 09:00 -- 09:30 | Musard Balliu On Specification and Verification of Information Flow Policies |
| 09:30 -- 10:00 | Simon Greiner Non-Interference in Component-Based Systems |
| 10:00 -- 10:30 | Daniel Bruns Verification of Secure Information Flow in Concurrent Programs |
| 10:30 -- 11:00 | Coffee break |
| 11:00 -- 11:30 | Vladimir Klebanov Pseudo-Random Number Generator Verification |
| 11:30 -- 11:50 | Stefan Mitsch Verified Runtime Validation and Proof-Aware Refactoring for Hybrid Systems |
| 12:00 -- 13:30 | Lunch break |
| 13:30 -- 14:00 | Martin Hentschel Current State of the KeY-Based Eclipse Projects |
| 14:00 -- 14:30 | Sarah Grebing Interative Software Verification -- Modeling the User in the Process |
| 14:30 -- 15:00 | Discussion: Target group(s), KeY as productivity tool? |
| 15:00 -- 15:30 | Coffee break |
| 15:30 -- 17:00 | Discussion: KeY book |
Time |
Topic |
| 09:30 -- 10:00 | Wojciech Mostowski Dynamic Frames Based Verification Method for Concurrent Java Programs |
| 10:00 -- 10:30 | Crystal Chang Din KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS |
| 10:30 -- 11:00 | Coffee break |
| 11:00 -- 11:50 | Discussion: Quo Vadis |
| 11:50 -- 12:00 | Wrap up |
| 12:00 -- 13:00 | Lunch |
| 13:00 | End of Symposium |