09:00‑10:00 Invited Talk
Location: IF G.07
| 09:00 | Bernhard Beckert Formal Verification of System Software |
10:20‑11:20 Session 4
Location: IF G.07
| 10:20 | Peter Schneider-Kamp Towards Complexity and Termination Analysis of Transition Systems |
| 10:40 | Peter Habermehl, Lukas Holik, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar A Proposal of a New Automata-based Representation of Heaps |
| 11:00 | Marius Bozga, Radu Iosif, Filip Konecny and Tomas Vojnar FLATA: Towards a Toolset for manipulation and analysis of counter automata |
11:20‑11:30 Mini Break of 10 Minutes
Location: IF G.07
11:30‑12:30 Session 5
Location: IF G.07
| 11:30 | Stefan Ratschan Verification of Mixed Discrete-Continuous Systems |
| 11:50 | Alejandro Sanchez and Cesar Sanchez Towards Temporal Verification of Concurrent Data-structures: In Need for Sophisticated Decision Procedures |
| 12:10 | Hossein Hojjat, Viktor Kuncak, Ruzica Piskac and Philippe Suter Vepar: A Framework for Automated Reasoning |
14:00‑15:00 Session 6
Location: IF G.07
| 14:00 | Paul Jackson and Grant Passmore Verification of Mixed Discrete-Continuous Systems |
| 14:20 | Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric RodrÃguez Carbonell and Albert Rubio Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic |
| 14:40 | Timothy Nelson, Dougherty Daniel, Kathi Fisler and Shriram Krishnamurthi On the Finite Model Property in Order-Sorted Logic |
15:20‑16:20 Session 7
Location: IF G.07
| 15:20 | Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic and Jovanka Pantovic Types for dynamic web data with RBAC |
| 15:40 | Predrag Janicic and Filip Maric Uniform reduction to SMT |
| 16:00 | Maria Paola Bonacina and Moa Johansson Advances in rewrite-based decision procedures |
16:20‑17:00 Closing Discussions
Location: IF G.07