Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Last revision Both sides next revision
program.txt [2011/02/24 10:56]
vkuncak created 		program.txt [2011/02/24 19:01]
vkuncak
Line 1: Line 1:
 ====== SVARM 2011 Program ====== ====== SVARM 2011 Program ======
  
-<​code>​ +Please see [[svarm11.pdf]].
- +
-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>​ +