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
rome13 [2013/01/15 15:58]
vkuncak
rome13 [2013/01/18 15:54] (current)
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]] and so do many flights.)
  
 ===== 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 ===
  
-<​code>​ +9:​00-10:​00 ​Invited Talk: **Francesco Ranzato - Complete Abstractions Everywhere** (shared with VMCAI) | 
- 9:​00-10:​00 ​VMCAI Invited Talk: Francesco Ranzato - Complete Abstractions Everywhere +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 +11:​00-11:​30 ​Hannes Mehnert: Unified Development and Verification of Java Programs in Eclipse ​| 
-11:00-11:30 Hannes Mehnert: Unified Development and Verification of Java Programs in Eclipse +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** (shared with VMCAI) | 
-14:00-15:00 Invited Talk: Joe Leslie-Hurd - Theory Engineering Using Composable Packages +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 +16:​00-16:​15 ​Break ^ 
-16:00-16:15 Break +16:​15-16:​45 ​Pavle Subotic: Automatic Compositional Analysis of Timed Automata ​| 
-16:15-16:45 Pavle Subotic: Automatic Compositional Analysis of Timed Automata +16:​45-17:​15 ​Predrag Janicic: Automated Generation of Formal and Readable Proofs of Mathematical Theorems ​| 
-16:45-17:15 Predrag Janicic: Automated Generation of Formal and Readable Proofs of Mathematical Theorems +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 ​Talk**Ken McMillan - Logic as the lingua franca of software verification** (shared with VMCAI) |
-18:00-19:00 Invited ​Speaker: Ken McMillan - Logic as the lingua franca of software verification +
-</​code>​+
  
 ===== General Information ===== ===== General Information =====
Line 44: 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 53: 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//