Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| svarm11:program [2011/04/12 08:57] – cesar.sanchez | svarm11:program [2011/04/12 18:14] (current) – cesar.sanchez | ||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | We will upload the slides for SVARM'11 here. | + | ====== Synthesis, Verification, |
| + | |||
| + | You can find the {{: | ||
| ====== Friday, April 1 ====== | ====== Friday, April 1 ====== | ||
| - | ^ 13:55 - 16:00 ^ ^ SESSION 1 ^ | + | ^ 13:55 - 16:00 ^ ^ SESSION 1 ^ ^ |
| - | | 13:55 | | Welcome | | + | | 13:55 | | Welcome |
| - | | 14:00 | Tom Henzinger (IST Austria) | Invited Talk: Quantitative reactive models | | + | | 14:00 | Tom Henzinger (IST Austria) | Invited Talk: Quantitative reactive models |
| - | | 15:00 | Adrian Francalanza | Reasoning about explicit resource management in message passing concurrency | + | | 15:00 | Adrian Francalanza | Reasoning about explicit resource management in message passing concurrency |
| - | | 15:20 | Radu Calinescu | Quantitative verification of adaptive IT systems | | + | | 15:20 | Radu Calinescu | Quantitative verification of adaptive IT systems |
| - | | 15:40 | Ran Ji | Provably correct compilation of an abstract behavioral modeling language | | + | | 15:40 | Ran Ji | Provably correct compilation of an abstract behavioral modeling language |
| | | | | | | | | | | ||
| - | ^16:00 - 16:30 ^ ** Coffee Break ** ^ ^ | + | ^16:00 - 16:30 ^ ** Coffee Break ** ^ ^ ^ |
| | | | | | | | | | | ||
| - | ^16:30 - 17:10 ^ ^ SESSION 2 ^ | + | ^16:30 - 17:10 ^ ^ SESSION 2 ^ ^ |
| - | | 16.30 | Jesper Bengtson | Separation logic for OO programs in Coq | | + | | 16.30 | Jesper Bengtson | Separation logic for OO programs in Coq | |
| - | | 16:50 | Jasmin Blanchette | Link between interactive and automated theorem provers | | + | | 16:50 | Jasmin Blanchette | Link between interactive and automated theorem provers |
| - | ^ 17:10 - 18:00 ^ Business Meeting ^ ^ | + | ^ 17:10 - 18:00 ^ Business Meeting |
| ====== Saturday, April 2 ====== | ====== Saturday, April 2 ====== | ||
| - | ^ 09:00 - 10:20 ^ ^ SESSION 3 ^ | + | ^ 09:00 - 10:20 ^ ^ SESSION 3 ^ ^ |
| - | | 09:00 | Philipp Ruemmer | Craig interpolation for integer arithmetic, uninterpreted functions, and the theory of arrays | | + | | 09:00 | Philipp Ruemmer | Craig interpolation for integer arithmetic, uninterpreted functions, and the theory of arrays |
| - | | 09:20 | Alessandro Armando | SMT-based symbolic model checking of administrative access control policies | | + | | 09:20 | Alessandro Armando | SMT-based symbolic model checking of administrative access control policies |
| - | | 09:40 | Eran Yahav |Synthesis of memory fences {{: | + | | 09:40 | Eran Yahav |Synthesis of memory fences |
| - | | 10.00 | Peter Schneide-Kamp | + | | 10:00 | | | | |
| - | | | | | | + | | | | | | |
| - | ^ 10:30 - 11:00 ^ ** Coffee Break ** ^ ^ | + | ^ 10:30 - 11:00 ^ ** Coffee Break ** ^ ^ ^ |
| - | | | | | | + | | | | | | |
| - | ^ 11:00 - 12:30 ^ ^ SESSION 4 ^ | + | ^ 11:00 - 12:30 ^ ^ SESSION 4 ^ ^ |
| - | | 11:00 | Aliaksei Tsitovich |From constructive to inductive proofs of termination | | + | | 11:00 | Aliaksei Tsitovich |From constructive to inductive proofs of termination |
| - | | 11:20 | Chantal Keller |Cooperation between SAT, | + | | 11:20 | Chantal Keller |Cooperation between SAT, |
| - | | 11:40 | Tayssir Touili | On model checking networks of pushdown systems | | + | | 11:40 | Tayssir Touili | On model checking networks of pushdown systems |
| - | | 12:00 | | Open mike for short research presentations | | + | | 12:00 | | Open mike for short research presentations |
| - | | | | | | + | | | | | | |
| - | ^ 12:30 -14:00 ^ ** Lunch ** ^ ^ | + | ^ 12:30 -14:00 ^ ** Lunch ** ^ ^ ^ |
| - | | | | | | + | | | | | | |
| - | ^ 14:00 - 16:00 ^ ^ SESSION 5 ^ | + | ^ 14:00 - 16:00 ^ ^ SESSION 5 ^ ^ |
| - | | 14:00 | George Candea | Invited Talk: S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems | | + | | 14:00 | George Candea | Invited Talk: S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems |
| - | | 15:00 | Radu Iosif | Numerical Transition Systems Competition | | + | | 15:00 | Radu Iosif | Numerical Transition Systems Competition |
| - | | | | | | + | | | | | | |
| - | ^ 16:00 - 16:30 ^ ** Coffee Break ** ^ ^ | + | ^ 16:00 - 16:30 ^ ** Coffee Break ** ^ ^ ^ |
| - | | | | | | + | | | | | | |
| - | ^ 16:30 - 17:30 ^ ^ SESSION 6 ^ | + | ^ 16:30 - 17:30 ^ ^ SESSION 6 ^ ^ |
| - | | 16:30 | Tomáš Vojnar | Two new tool prototypes for shape analysis | | + | | 16:30 | Tomáš Vojnar | Two new tool prototypes for shape analysis |
| - | | 16:50 | Alejandro Sánchez | Deductive Temporal Verification of Parametrized Concurrent Systems | | + | | 16:50 | Alejandro Sánchez | Deductive Temporal Verification of Parametrized Concurrent Systems |
| - | | 17:10 | Filip Maric | Verified efficient unsatisfiability proof checking for SAT | | + | | 17:10 | Filip Maric | Verified efficient unsatisfiability proof checking for SAT | {{: |
| ====== Sunday, April 3 ====== | ====== Sunday, April 3 ====== | ||
| - | ^ 09:00 - 10:20 ^ ^ SESSION 7 ^ | + | ^ 09:00 - 10:20 ^ ^ SESSION 7 ^ ^ |
| - | | 09:00 | Darko Marinov | Invited talk: Systematic Software Testing Using Test Abstractions | | + | | 09:00 | Darko Marinov | Invited talk: Systematic Software Testing Using Test Abstractions |
| - | | 10:00 | Tuomas Launiainen | Efficient model checking of PSL safety properties | | + | | 10:00 | Tuomas Launiainen | Efficient model checking of PSL safety properties |
| - | | | | | | + | | | | | | |
| - | ^ 10:30 - 11:00 ^ ** Coffee Break ** ^ ^ | + | ^ 10:30 - 11:00 ^ ** Coffee Break ** ^ ^ ^ |
| - | | | | | | + | | | | | | |
| - | ^ 11:00 - 12:20 ^ ^ SESSION 8 ^ | + | ^ 11:00 - 12:20 ^ ^ SESSION 8 ^ ^ |
| - | | 11:00| Denis Trček | On Rich Models Issues for Trust Management & Qualitative Algebra | | + | | 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 | | + | | 11:20| Christian von Essen | Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives |
| - | | 11:40| Alexis Marechal | Verifying Design Patterns using Symbolic Model Checking | | + | | 11:40| Alexis Marechal | Verifying Design Patterns using Symbolic Model Checking |
| - | | 12:00| Stefan Ratschan | Numerical constraint solving based on linear relaxations | | + | | 12:00| Stefan Ratschan | Numerical constraint solving based on linear relaxations |
| - | | | | | | + | | | | | | |
| - | ^ 12:30 - 14:00 ^ ** Lunch ** ^ ^ | + | ^ 12:30 - 14:00 ^ ** Lunch ** ^ ^ ^ |
| - | | | | | | + | | | | | | |
| - | ^ 14:00 - 16:00 ^ ^ SESSION 9 ^ | + | ^ 14:00 - 16:00 ^ ^ SESSION 9 ^ ^ |
| - | | 14:00 | Ruslán Garza | Analysis and Verification of Higher Order Functional Programs: An Automata Theoretic Approach | | + | | 14:00 | Ruslán |
| - | | 14:20 | Johannes Kinder | Static Analysis of x86 Executables | | + | | 14:20 | Johannes Kinder | Static Analysis of x86 Executables |
| - | | 14:40 | Ruzica Piskac | Software Synthesis using Automated Reasoning | | + | | 14:40 | Ruzica Piskac | Software Synthesis using Automated Reasoning |
| - | | 15:00 | Rupak Majumdar | Invited talk: Verification for control | | + | | 15:00 | Rupak Majumdar | Invited talk: Verification for control |
| - | | | | | | + | | | | | | |
| - | ^ 16:00 - 16:30 ^ ** Coffee Break ** ^ ^ | + | ^ 16:00 - 16:30 ^ ** Coffee Break ** ^ ^ ^ |
| - | | | | | | + | | | | | | |
| - | ^ 16:30 - 18:00 ^ ^ SESSION 10 ^ | + | ^ 16:30 - 18:00 ^ ^ SESSION 10 ^ ^ |
| - | | | | Open Discussions on Future Collaboration Steps | | + | | | | Open Discussions on Future Collaboration Steps | | |