Synthesis, Verification, and Analysis of Rich Models (SVARM 2011)
| 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 | |