Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Last revision Both sides next revision
rome13 [2013/01/15 16:00]
vkuncak
rome13 [2013/01/18 15:53]
vkuncak
Line 1: Line 1:
 ====== Workshop on Synthesis, Verification and Analysis of Rich Models: Rome, 20-21 January 2013 ====== ====== Workshop on Synthesis, Verification and Analysis of Rich Models: Rome, 20-21 January 2013 ======
 +
 +Location: [[http://​www.robertonaldicollection.com/​eng/​parco_dei_principi/​hotel_luxury_rome_parioli.htm|Hotel Parco Dei Principi]], Via G. Frescobaldi,​ 5 - 00198 Rome, Italy, [[http://​popl13.di.univr.it/​styled-10/​styled-9/​files/​download-the-map.pdf|Room Sforza A]]
 +
 +[[http://​popl13.di.univr.it/​index.html|Omniae viae ferunt Romam]]
  
 ===== PROGRAM ===== ===== PROGRAM =====
Line 5: Line 9:
 === Sunday, 20 January 2013 === === Sunday, 20 January 2013 ===
  
-| 9:​00-10:​00 ​ | (VMCAI) ​Invited Talk: **Leonardo de Moura - A Model-Constructing Satisfiability Calculus** |+| 9:​00-10:​00 ​ | Invited Talk: **Leonardo de Moura - A Model-Constructing Satisfiability Calculus** ​(shared with VMCAI) ​|
 ^ 10:00-10:30 ^ Break ^ ^ 10:00-10:30 ^ Break ^
 | 10:30-11:00 | Serdar Erbatur: Unification in Blind Signatures |  | 10:30-11:00 | Serdar Erbatur: Unification in Blind Signatures | 
Line 11: Line 15:
 | 11:30-12:00 | Stefan Ratschan: Nelson-Oppen with a Quasi-decidable Logical Theory | | 11:30-12:00 | Stefan Ratschan: Nelson-Oppen with a Quasi-decidable Logical Theory |
 ^ 12:00-14:00 ^ Lunch ^ ^ 12:00-14:00 ^ Lunch ^
-| 14:00-15:00 | (VMCAI) ​Invited Talk: **Eran Yahav - Abstraction-Guided Synthesis** |+| 14:00-15:00 | Invited Talk: **Eran Yahav - Abstraction-Guided Synthesis** ​(shared with VMCAI) ​|
 | 15:00-15:30 | Eva Darulova: Certified numerical computation | | 15:00-15:30 | Eva Darulova: Certified numerical computation |
 | 15:30-16:00 | Denis Firsov: Certified normalization of context-free grammars and CYK parsing | | 15:30-16:00 | Denis Firsov: Certified normalization of context-free grammars and CYK parsing |
 ^ 16:00-16:30 ^ Break ^ ^ 16:00-16:30 ^ Break ^
 | 16:30-17:00 | Yaron Welner: Games on Graphs with Robust Quantitative Objectives: Decidability and Complexity Analysis | | 16:30-17:00 | Yaron Welner: Games on Graphs with Robust Quantitative Objectives: Decidability and Complexity Analysis |
-| 17:00-18:30 | Management Committee meeting ​(for COST only) |+| 17:00-18:30 | Management Committee meeting ​ |
  
 === Monday, 21 January 2013 === === Monday, 21 January 2013 ===
  
-| 9:00-10:00 | VMCAI Invited Talk: **Francesco Ranzato - Complete Abstractions Everywhere** |+| 9:00-10:00 | Invited Talk: **Francesco Ranzato - Complete Abstractions Everywhere** ​(shared with VMCAI) ​|
 ^ 10:00-10:30 ^ Break ^ ^ 10:00-10:30 ^ Break ^
 | 10:30-11:00 | Mnacho Echenim: On an abductive approach to error detection | | 10:30-11:00 | Mnacho Echenim: On an abductive approach to error detection |
Line 26: Line 30:
 | 11:30-12:00 | Mark Micallef: The Equivalent Mutant Problem in Mutation Testing | | 11:30-12:00 | Mark Micallef: The Equivalent Mutant Problem in Mutation Testing |
 ^ 12:00-14:00 ^ Lunch ^ ^ 12:00-14:00 ^ Lunch ^
-| 14:00-15:00 | Invited Talk: **Joe Leslie-Hurd - Theory Engineering Using Composable Packages** |+| 14:00-15:00 | Invited Talk: **Joe Leslie-Hurd - Theory Engineering Using Composable Packages** ​(shared with VMCAI) ​|
 | 15:00-15:30 | Markus Rabe: A logic for hyperproperties | | 15:00-15:30 | Markus Rabe: A logic for hyperproperties |
 | 15:30-16:00 | Hossein Hojjat: Combining Infinite-state Verification Techniques in Analyzing Integer Models | | 15:30-16:00 | Hossein Hojjat: Combining Infinite-state Verification Techniques in Analyzing Integer Models |
Line 34: Line 38:
 | 17:15-17:45 | Daniel Larraz: Proving termination of C-like programs using MAX-SMT | | 17:15-17:45 | Daniel Larraz: Proving termination of C-like programs using MAX-SMT |
 ^ 17:45-18:00 ^ Break ^ ^ 17:45-18:00 ^ Break ^
-| 18:00-19:00 | Invited ​Speaker: **Ken McMillan - Logic as the lingua franca of software verification** |+| 18:00-19:00 | Invited ​Talk: **Ken McMillan - Logic as the lingua franca of software verification** ​(shared with VMCAI) ​|
  
 ===== General Information ===== ===== General Information =====
Line 42: Line 46:
 This workshop also serves as the meeting of the Rich Model Toolkit COST Action IC0901. Information about the Action: http://​richmodels.epfl.ch/​ This workshop also serves as the meeting of the Rich Model Toolkit COST Action IC0901. Information about the Action: http://​richmodels.epfl.ch/​
  
-The meeting continues a series of meetings held in Brussels, Belgrade, Edinburgh, Lugano, Saarbruecken,​ Dagstuhl, Turin, Tallinn, Manchester, and Haifa held in the period 2009-2012.+The meeting continues a series of meetings held in Brussels, Belgrade, Edinburgh, Lugano, Saarbruecken,​ Dagstuhl, Turin, Tallinn, Trento, Manchester, and Haifa held in the period 2009-2012.
  
 ===== Local Arrangements ===== ===== Local Arrangements =====
Line 51: Line 55:
  
 We are pleased to confirm keynotes from: We are pleased to confirm keynotes from:
-  * **[[http://​www.kenmcmil.com/​|Kenneth L. McMillan]]** (Microsoft Research)+  * **[[http://​www.kenmcmil.com/​|Kenneth L. McMillan]]** (Microsoft Research): //Logic as the lingua franca of software verification//​
   * **[[http://​www.gilith.com/​about/​|Joe Leslie-Hurd]]** (Intel): //Theory Engineering Using Composable Packages//   * **[[http://​www.gilith.com/​about/​|Joe Leslie-Hurd]]** (Intel): //Theory Engineering Using Composable Packages//