This is an old revision of the document!

A PCRE internal error occured. This might be caused by a faulty plugin

====== SVARM 2011 Program ====== <code> April 1 1:55: Welcome 2-3 Invited Talk: Tom Henzinger: Quantitative reactive models 3-3:30 break 3:30-5 4 talks Adrian Francalanza: Reasoning about explicit resource management in message passing concurrency Radu Calinescu: Quantitative verification of adaptive IT systems Reiner Hähnle: Provably correct compilation of an abstract behavioral modeling language Lars Birkedal: Separation logic for OO programs in Coq 5- Management meeting April 2 9-10 3 talks Jasmin Blanchette: Link between interactive and automated theorem provers Philipp Ruemmer: Craig interpolation for integer arithmetic, uninterpreted functions, and the theory of arrays Alessandro Armando: SMT-based symbolic model checking of administrative access control policies 10 - 1030 break 1030-1210 5 talks Eran Yahav: Synthesis of memory fences Peter Schneide-Kamp: Lazy abstraction for size-change termination Aliaksei Tsitovich: From constructive to inductive proofs of termination Hugo Herberlin: Certifying C programs Tayssir Touili: On model checking networks of pushdown systems 1215-1230: Open mike for short research presentations 1230-2 lunch 2-3 Invited Talk: George Candea: S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems 3-4 break, and Numerical Transition Systems Competition (Radu Iosif) 4-5 3 talks Tomas Vojnar: Two new tool prototypes for shape analysis Alejandro Sanchez: Deductive Temporal Verification of Parametrized Concurrent Systems Filip Maric: Verified efficient unsatisfiability proof checking for SAT April 3 9-10 Invited talk: Darko Marinov: Systematic Software Testing Using Test Abstractions 10-1030 break 1030-1210: 5 talks Tuomas Launiainen: Efficient model checking of PSL safety properties Denis Treek: Qualitative algebra for trust management Christian von Essen: Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives Alexis Marechal: Verifying Design Patterns using Symbolic Model Checking Stefan Ratschan: Numerical constraint solving based on linear relaxations 1215-1230: Open mike for short research presentations 1230-2 lunch 2-3:20 4 talks Ruslan Garza: Analysis and Verification of Higher Order Functional Programs: An Automata Theoretic Approach Johannes Kinder: Static Analysis of x86 Executables Ruzica Piskac: Software Synthesis using Automated Reasoning Rupak Majumdar: Verification for control 3:20-4:00 Break 4-5: Open Discussions on Future Collaboration Steps </code>