10th KeY Symposium 2011 -- Programme
Last modification: $Date: 2011/07/08 08:59:35 $(GMT)
Friday, 26th Aug
Time |
Topic |
Session |
| 9:00 -- 10:00 | Invited Talk:
Verification of Concurrent Data Structures Marieke Huisman |
|
| 10:00 -- 10:30 |
Broadening the scope of the Java Modeling Language through Java Annotations James Hunt |
Specification |
| 10:30 -- 11:00 | Coffee Break | |
| 11:00 -- 11:30 | Improving the usability of specification languages and methods for annotation-based verification Bernhard Beckert, Vladimir Klebanov, Thorsten Bormer | |
| 11:30 -- 12:00 | Formal semantics of model fields inspired by a generalization of Hilbert's epsilon terms Bernhard Beckert, Daniel Bruns | |
| 12:00 -- 12:30 | Specification of red-black trees: Showcasing dynamic frames, model fields and sequences Daniel Bruns | |
| 12:30 -- 14:00 | Lunch | |
| 14:00 -- 14:30 | Verification of Alloy models using KeY Ulrich Geilmann | Verification |
| 14:30 -- 15:00 | Visualizing Deductive Software Design Martin Hentschel, Ina Schaefer | |
| 15:00 -- 15:30 | Proving the satisfiability of first-order logic formulas -work in progress- Christoph Gladisch | |
| 15:30 -- 15:45 | Ensuring the correctness of user-defined rules based on
first-order logic in the KeY system Benjamin Niedermann | |
| 15:45 -- 16:15 | Coffee Break | |
| 16:15 -- 16:45 | Verified resource guarantees for heap manipulating programs Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, German Puebla, Guillermo Roman Diez | Resources |
| 16:45 -- 17:15 | Verified heap bounds in Java Olha Shkaravska, Marko van Eekelen | |
| 17:15 -- 17:45 | Ranking functions for loops with disjunctive exit-conditions Rody Kersten, Marko van Eekelen | |
| Evening | Workshop Dinner |
Saturday, 27th August
Time |
Topic |
Session |
| 09:00 -- 9:30 | CHARTER - Combining KeY with complementary tools for certification James Hunt | Certification |
| 9:30 -- 10:00 | Minding the gap in KeY proof certificates Gabriele Paganelli, Wolfgang Ahrendt | |
| 10:00 -- 10:30 | VeriFlux: A data-flow analysis tool for realtime Java Isabel Tonin, James Hunt | |
| 10:30 -- 11:00 | Coffee Break | |
| 11:00 -- 11:30 | Verification of information-flow properties of Java programs Christoph Scheben | Information-Flow |
| 11:30 -- 12:00 | Quantifying information-flow with KeY Vladimir Klebanov | |
| 12:00 -- 12:30 | An abstract framework for an object-oriented dynamic logic
with information-flow analysis Bart van Delft | |
| 12:30 -- 14:00 | Lunch | |
| 14:00 -- 14:30 | Algorithmic refinement from pseudo code to code Mattias Ulbrich | Refinement and Compilation |
| 14:30 -- 15:00 | Towards deductive compilation Ran Ji | |
| 15:00 -- 15:45 | Demo/New Feature/KeY 2.0 preview (Planned) | |
| 15:45 -- | Good-Bye and Coffee |