You can find the Meeting Program in pdf format.
| 13:55 - 16:00 | SESSION 1 | ||
|---|---|---|---|
| 13:55 | Welcome | ||
| 14:00 | Tom Henzinger (IST Austria) | Invited Talk: Quantitative reactive models | |
| 15:00 | Adrian Francalanza | Reasoning about explicit resource management in message passing concurrency | slides |
| 15:20 | Radu Calinescu | Quantitative verification of adaptive IT systems | slides |
| 15:40 | Ran Ji | Provably correct compilation of an abstract behavioral modeling language | slides |
| 16:00 - 16:30 | Coffee Break | ||
| 16:30 - 17:10 | SESSION 2 | ||
| 16.30 | Jesper Bengtson | Separation logic for OO programs in Coq | |
| 16:50 | Jasmin Blanchette | Link between interactive and automated theorem provers | slides |
| 17:10 - 18:00 | Business Meeting |
| 09:00 - 10:20 | SESSION 3 | ||
|---|---|---|---|
| 09:00 | Philipp Ruemmer | Craig interpolation for integer arithmetic, uninterpreted functions, and the theory of arrays | slides |
| 09:20 | Alessandro Armando | SMT-based symbolic model checking of administrative access control policies | slides |
| 09:40 | Eran Yahav | Synthesis of memory fences | slides |
| 10:00 | |||
| 10:30 - 11:00 | Coffee Break | ||
| 11:00 - 12:30 | SESSION 4 | ||
| 11:00 | Aliaksei Tsitovich | From constructive to inductive proofs of termination | slides |
| 11:20 | Chantal Keller | Cooperation between SAT, SMT provers and Coq | slides |
| 11:40 | Tayssir Touili | On model checking networks of pushdown systems | |
| 12:00 | Open mike for short research presentations | ||
| 12:30 -14:00 | Lunch | ||
| 14:00 - 16:00 | SESSION 5 | ||
| 14:00 | George Candea | Invited Talk: S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems | slides |
| 15:00 | Radu Iosif | Numerical Transition Systems Competition | slides |
| 16:00 - 16:30 | Coffee Break | ||
| 16:30 - 17:30 | SESSION 6 | ||
| 16:30 | Tomáš Vojnar | Two new tool prototypes for shape analysis | slides |
| 16:50 | Alejandro Sánchez | Deductive Temporal Verification of Parametrized Concurrent Systems | slides |
| 17:10 | Filip Maric | Verified efficient unsatisfiability proof checking for SAT | slides |
| 09:00 - 10:20 | SESSION 7 | ||
|---|---|---|---|
| 09:00 | Darko Marinov | Invited talk: Systematic Software Testing Using Test Abstractions | |
| 10:00 | Tuomas Launiainen | Efficient model checking of PSL safety properties | slides |
| 10:30 - 11:00 | Coffee Break | ||
| 11:00 - 12:20 | SESSION 8 | ||
| 11:00 | Denis Trček | On Rich Models Issues for Trust Management & Qualitative Algebra | |
| 11:20 | Christian von Essen | Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives | slides |
| 11:40 | Alexis Marechal | Verifying Design Patterns using Symbolic Model Checking | slides |
| 12:00 | Stefan Ratschan | Numerical constraint solving based on linear relaxations | slides |
| 12:30 - 14:00 | Lunch | ||
| 14:00 - 16:00 | SESSION 9 | ||
| 14:00 | Ruslán Ledesma Garza | Analysis and Verification of Higher Order Functional Programs: An Automata Theoretic Approach | slides |
| 14:20 | Johannes Kinder | Static Analysis of x86 Executables | |
| 14:40 | Ruzica Piskac | Software Synthesis using Automated Reasoning | slides |
| 15:00 | Rupak Majumdar | Invited talk: Verification for control | |
| 16:00 - 16:30 | Coffee Break | ||
| 16:30 - 18:00 | SESSION 10 | ||
| Open Discussions on Future Collaboration Steps |