====== Synthesis, Verification, and Analysis of Rich Models (SVARM 2011) ======

You can find the {{:svarm2011.pdf|Meeting Program}} in pdf format.


====== Friday, April 1 ======

^ 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  | {{:svarm11:francalanzaslides.pdf|slides}} |
| 15:20 | Radu Calinescu | Quantitative verification of adaptive IT systems | {{:svarm11:calinescuslides.pdf|slides}} |
| 15:40 | Ran Ji | Provably correct compilation of an abstract behavioral modeling language | {{:svarm11:svarm-ran.pdf|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 | {{:svarm11:svarm2011-sledge.pdf|slides}}|
^ 17:10 - 18:00 ^ Business Meeting ^ ^ ^


====== Saturday, April 2 ======

^ 09:00 - 10:20 ^ ^ SESSION 3 ^ ^
| 09:00 | Philipp Ruemmer | Craig interpolation for integer arithmetic, uninterpreted functions, and the theory of arrays | {{:svarm11:slides-philipp-ruemmer.pdf|slides}}|
| 09:20 | Alessandro Armando | SMT-based symbolic model checking of administrative access control policies | {{:svarm11:armandotalk-svarm11.pdf|slides}}|
| 09:40 | Eran Yahav |Synthesis of memory fences | {{:svarm11:yahavslides.pptx|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 | {{:svarm11:svarm11_slides_tsitovich.pdf|slides}} |
| 11:20 | Chantal Keller |Cooperation between SAT, SMT provers and Coq | {{:svarm11:kellersvarm11.pdf|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 | {{:svarm11:svarm_candea.pdf|slides}}|
| 15:00 | Radu Iosif | Numerical Transition Systems Competition | {{:svarm11:iosifnts-slide.pdf|slides}}|
| | | | |
^ 16:00 - 16:30 ^ ** Coffee Break ** ^ ^ ^
| | | | |
^ 16:30 - 17:30 ^ ^ SESSION 6 ^ ^
| 16:30 | Tomáš Vojnar | Two new tool prototypes for shape analysis | {{:svarm11:vojnarsvarm11.pdf|slides}} |
| 16:50 | Alejandro Sánchez | Deductive Temporal Verification of Parametrized Concurrent Systems | {{:svarm11:sanchezsvarm11.pdf|slides}}|
| 17:10 | Filip Maric | Verified efficient unsatisfiability proof checking for SAT | {{:svarm11:filipslides.pdf|slides}} |


====== Sunday, April 3 ======

^ 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 | {{:svarm11:tuomasslides.pdf|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 |{{:svarm11:vonessentalk.pdf|slides}} |
| 11:40| Alexis Marechal | Verifying Design Patterns using Symbolic Model Checking | {{:svarm11:marechalmain.pdf|slides}}|
| 12:00| Stefan Ratschan | Numerical constraint solving based on linear relaxations | {{:svarm11:ratschan.pdf|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 | {{:svarm11:garzasvarm11.pdf|slides}} |
| 14:20 | Johannes Kinder | Static Analysis of x86 Executables | |
| 14:40 | Ruzica Piskac | Software Synthesis using Automated Reasoning |{{:svarm11:ruzicapiskac.ppt|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 | |