Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
svarm11:program [2011/04/12 14:01] – cesar.sanchezsvarm11:program [2011/04/12 18:14] (current) – cesar.sanchez
Line 1: Line 1:
-We will upload the slides for SVARM'11 here.+====== Synthesis, Verification, and Analysis of Rich Models (SVARM 2011) ====== 
 + 
 +You can find the {{:svarm2011.pdf|Meeting Program}} in pdf format. 
  
 ====== Friday, April 1 ====== ====== Friday, April 1 ======
Line 20: Line 23:
 ====== 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 | {{:svarm11:slides-philipp-ruemmer.pdf|slides}}| 
-| 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 | {{:svarm11:armandotalk-svarm11.pdf|slides}}| 
-| 09:40 | Eran Yahav |Synthesis of memory fences {{:svarm11:yahavslides.pptx|slides}} | +| 09:40 | Eran Yahav |Synthesis of memory fences | {{:svarm11:yahavslides.pptx|slides}} | 
-| 10.00 | Peter Schneide-Kamp | Lazy abstraction for size-change termination | +| 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 | {{:svarm11:svarm11_slides_tsitovich.pdf|slides}} | 
-| 11:20 | Chantal Keller |Cooperation between SAT, SMT provers and Coq | +| 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 | +| 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 | {{:svarm11:svarm_candea.pdf|slides}}| 
-| 15:00 | Radu Iosif | Numerical Transition Systems Competition | +| 15:00 | Radu Iosif | Numerical Transition Systems Competition | {{:svarm11:iosifnts-slide.pdf|slides}}| 
-| | | | +| | | | | 
-^ 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 | {{:svarm11:vojnarsvarm11.pdf|slides}} | 
-| 16:50 | Alejandro Sánchez | Deductive Temporal Verification of Parametrized Concurrent Systems | +| 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 |+| 17:10 | Filip Maric | Verified efficient unsatisfiability proof checking for SAT | {{:svarm11:filipslides.pdf|slides}} |
  
  
 ====== 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 | {{:svarm11:tuomasslides.pdf|slides}} | 
-| | | | +| | | | | 
-^ 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 |{{:svarm11:vonessentalk.pdf|slides}} | 
-| 11:40| Alexis Marechal | Verifying Design Patterns using Symbolic Model Checking | +| 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 | +| 12:00| Stefan Ratschan | Numerical constraint solving based on linear relaxations | {{:svarm11:ratschan.pdf|slides}}| 
-| | | |  +| | | | | 
-^ 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 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: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 |{{:svarm11:ruzicapiskac.ppt|slides}} | 
-| 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 | |