Last Update: 2016-08-30 11:37 AM
|
Topic |
Start Time |
End Time |
Name |
Talk Title |
Duration |
|||
|
05:30 PM |
06:00 PM |
Welcome |
00:30:00 |
Monday |
||||
|
06:00 PM |
07:00 PM |
Dinner |
01:00:00 |
|||||
|
KeY Features |
07:00 PM |
07:20 PM |
Martin Hentschel (substituted by Richard Bubel) |
Current status of the KeY Eclipse integration |
00:20:00 |
|||
|
Discussions |
07:20 PM |
07:50 PM |
Discussion in breakout groups: 3
|
00:30:00 |
||||
|
07:50 PM |
08:20 PM |
Presentation of results, plenum discussion |
00:30:00 |
|||||
|
07:30 AM |
09:30 AM |
Breakfast |
02:00:00 |
Tuesday |
||||
|
Invited Talk |
09:30 AM |
10:30 AM |
Carlo A. Furia |
01:00:00 1 |
||||
|
Security |
10:30 AM |
11:00 AM |
Simon Greiner |
(Enforcing Non-Interference in component-based Systems) 2 |
00:30:00 |
|||
|
11:00 AM |
11:30 AM |
Coffee break |
00:30:00 |
|||||
|
11:30 AM |
12:00 PM |
Alexander Weigl |
Efficient SAT-based Pre-image Enumeration for Quantifying Information Flow in Programs |
00:30:00 |
||||
|
12:00 PM |
12:30 PM |
Quoc Huy Do |
Inferring Secrets by Guided Experiments |
00:30:00 |
||||
|
12:30 PM |
01:30 PM |
Lunch |
01:00:00 |
|||||
|
01:30 PM |
02:00 PM |
Vladimir Klebanov |
(Security / Information Flow) 2 |
00:30:00 |
||||
|
02:00 PM |
02:30 PM |
Michael Kirsten |
Automated Verification for Functional and Relational Properties of Voting Rules |
00:30:00 |
||||
|
Beyond KeY |
02:30 PM |
02:45 PM |
Stefan Mitsch |
KeYmaera X: Tactics and Proof-By-Pointing |
00:15:00 |
|||
|
02:45 PM |
03:15 PM |
Thomas Baar |
00:30:00 |
|||||
|
04:00 PM |
Open End |
Social Event and Barbeque |
||||||
|
07:30 AM |
09:00 AM |
Breakfast |
01:30:00 |
Wednesday |
||||
|
Applicability and Usability |
09:00 AM |
10:00 AM |
Reiner Hähnle |
Can Formal Methods Improve the Efficiency of Code Reviews? |
01:00:00 1 |
|||
|
10:00 AM |
10:30 AM |
Sarah Grebing |
Bridging the Interaction Gap between Code and Logic |
00:30:00 |
||||
|
10:30 AM |
11:00 AM |
Coffee break |
00:30:00 |
|||||
|
Case Studies |
11:00 AM |
11:30 AM |
Jonas Schiffl |
00:30:00 |
||||
|
11:30 AM |
12:00 PM |
Eduard Kamburjan |
Session Types for ABS |
00:30:00 |
||||
|
12:00 PM |
12:15 PM |
Eduard Kamburjan |
Modeling Railways with ABS and KeY-ABS |
00:15:00 |
||||
|
12:15 PM |
12:30 PM |
Stijn de Gouw |
|
00:15:00 |
||||
|
12:30 PM |
01:30 PM |
Lunch |
01:00:00 |
|||||
|
01:30 PM |
02:00 PM |
Mihai Herda |
Case Study: Verification of a Mix-Server |
00:30:00 |
||||
|
02:00 PM |
02:30 PM |
Marko Kleine Büning |
Combining Graph-Based Information-Flow Analysis with KeY for Proving Non-Interference |
00:30:00 |
||||
|
02:30 PM |
02:45 PM |
Short Break |
00:15:00 |
|||||
|
Extensions to the KeY Logic |
02:45 PM |
03:15 PM |
Peter H. Schmitt |
00:30:00 |
||||
| Beyond KeY |
03:15 PM |
03:30 PM |
Abel Garcia |
KeY-aided deadlock analysis2 |
00:15:00 |
|||
|
03:30 PM |
04:00 PM |
Coffee break |
00:30:00 |
|||||
|
04:00 PM |
04:30 PM |
Tianxiang Dr. Lu |
What is TLA+? |
00:30:00 |
||||
| Extensions to the KeY Logic |
04:30 PM |
04:45 PM |
Nathan Wasser |
(Loop invariant Soundness with Abrupt Termination) |
00:15:00 |
|||
|
Specification Generation |
04:45 PM |
05:15 PM |
Nathan Wasser |
(Automatic Specification Generation) 2 |
00:30:00 |
|||
|
05:15 PM |
05:30 PM |
Short Break |
00:15:00 |
|||||
|
05:30 PM |
06:00 PM |
Simon Robillard |
When provers help provers: possible interactions between Key and Vampire |
00:30:00 |
||||
|
06:00 PM |
06:15 PM |
YuTing Jeff Chen |
Theory-Specific Reasoning about Loops with Arrays using Vampire |
00:15:00 |
||||
|
06:30 PM |
Dinner |
|||||||
|
Meeting of the KeY book editors |
||||||||
|
07:30 AM |
10:00 AM |
Breakfast |
02:30:00 |
Thursday |
||||
|
Check-out and cleaning of rooms and common areas except for the seminar room |
||||||||
|
Relational Verification |
10:00 AM |
10:15 AM |
Mattias Ulbrich |
00:15:00 |
||||
|
10:15 AM |
10:45 AM |
Moritz Kiefer |
00:30:00 |
|||||
|
10:45 AM |
11:15 AM |
Stephan Gocht |
00:30:00 |
|||||
|
11:30 AM |
Cleaning of the seminar room, Good-Bye |
|||||||