Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
program.txt [2011/02/24 10:56] vkuncak created |
program.txt [2011/02/24 19:02] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== SVARM 2011 Program ====== | ====== SVARM 2011 Program ====== | ||
- | <code> | + | Please see the {{:svarm2011.pdf|program as a pdf file}}. |
- | + | ||
- | 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> | + |