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
Next revision Both sides next revision
rome13 [2012/11/08 21:24]
vkuncak
rome13 [2013/01/18 15:51]
vkuncak
Line 1: Line 1:
-====== Workshop on Synthesis, Verification and Analysis of Rich Models: Rome 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]] 
 + 
 +===== PROGRAM ===== 
 + 
 +=== Sunday, 20 January 2013 === 
 + 
 +| 9:​00-10:​00 ​ | Invited Talk: **Leonardo de Moura - A Model-Constructing Satisfiability Calculus** (shared with VMCAI) | 
 +^ 10:00-10:30 ^ Break ^ 
 +| 10:30-11:00 | Serdar Erbatur: Unification in Blind Signatures |  
 +| 11:00-11:30 | Corneliu Popeea: On Solving Existentially Quantified Horn Clauses (and Proving CTL Properties of Programs) | 
 +| 11:30-12:00 | Stefan Ratschan: Nelson-Oppen with a Quasi-decidable Logical Theory | 
 +^ 12:00-14:00 ^ Lunch ^ 
 +| 14:00-15:00 | Invited Talk: **Eran Yahav - Abstraction-Guided Synthesis** (shared with VMCAI) | 
 +| 15:00-15:30 | Eva Darulova: Certified numerical computation | 
 +| 15:30-16:00 | Denis Firsov: Certified normalization of context-free grammars and CYK parsing | 
 +^ 16:00-16:30 ^ Break ^ 
 +| 16:30-17:00 | Yaron Welner: Games on Graphs with Robust Quantitative Objectives: Decidability and Complexity Analysis | 
 +| 17:00-18:30 | Management Committee meeting ​ | 
 + 
 +=== Monday, 21 January 2013 === 
 + 
 +| 9:00-10:00 | Invited Talk: **Francesco Ranzato - Complete Abstractions Everywhere** (shared with VMCAI) | 
 +^ 10:00-10:30 ^ Break ^ 
 +| 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:30-12:00 | Mark Micallef: The Equivalent Mutant Problem in Mutation Testing | 
 +^ 12:00-14:00 ^ Lunch ^ 
 +| 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:30-16:00 | Hossein Hojjat: Combining Infinite-state Verification Techniques in Analyzing Integer Models | 
 +^ 16:00-16:15 ^ Break ^ 
 +| 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 | 
 +| 17:15-17:45 | Daniel Larraz: Proving termination of C-like programs using MAX-SMT | 
 +^ 17:45-18:00 ^ Break ^ 
 +| 18:00-19:00 | Invited Talk: **Ken McMillan - Logic as the lingua franca of software verification** (shared with VMCAI) | 
 + 
 +===== General Information ​=====
  
 Meeting is collocated with [[http://​popl.mpi-sws.org/​2013/​|POPL 2013]], organized by **Maria Paola Bonacina** and **Cesar Sanchez**. Meeting is collocated with [[http://​popl.mpi-sws.org/​2013/​|POPL 2013]], organized by **Maria Paola Bonacina** and **Cesar Sanchez**.
Line 5: Line 44:
 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 ===== 
 + 
 +See [[http://​popl13.di.univr.it/​styled-2/​styled-7/​index.html|list of nearby hotels]].
  
 ===== KEYNOTES ===== ===== KEYNOTES =====
  
 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)+  * **[[http://​www.gilith.com/​about/​|Joe Leslie-Hurd]]** (Intel): //Theory Engineering Using Composable Packages//
  
 ===== Scope of the Event ===== ===== Scope of the Event =====