Differences

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

--- rome13 [2013/01/15 15:53] – 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 ======
+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 =====
@@ Line 5: / Line 9: @@
 === Sunday, 20 January 2013 ===
-<code>
+| 9:00-10:00  | Invited Talk: **Leonardo de Moura - A Model-Constructing Satisfiability Calculus** (shared with VMCAI) |
-:00-10:00 VMCAI Invited Talk: Leonardo de Moura - A Model-Constructing Satisfiability Calculus
+^ 10:00-10:30 ^ Break ^
-:00-10:30 Break
+| 10:30-11:00 | Serdar Erbatur: Unification in Blind Signatures |
-: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) |
-: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 |
-:30-12:00 Stefan Ratschan: Nelson-Oppen with a Quasi-decidable Logical Theory
+^ 12:00-14:00 ^ Lunch ^
-:00-14:00 Lunch
+| 14:00-15:00 | Invited Talk: **Eran Yahav - Abstraction-Guided Synthesis** (shared with VMCAI) |
-:00-15:00 VMCAI Invited Talk: Eran Yahav - Abstraction-Guided Synthesis
+| 15:00-15:30 | Eva Darulova: Certified numerical computation |
-:00-15:30 Eva Darulova: Certified numerical computation
+| 15:30-16:00 | Denis Firsov: Certified normalization of context-free grammars and CYK parsing |
-:30-16:00 Denis Firsov: Certified normalization of context-free grammars and CYK parsing
+^ 16:00-16:30 ^ Break ^
-:00-16:30 Break
+| 16:30-17:00 | Yaron Welner: Games on Graphs with Robust Quantitative Objectives: Decidability and Complexity Analysis |
-:30-17:00 Yaron Welner: Games on Graphs with Robust Quantitative Objectives:
+| 17:00-18:30 | Management Committee meeting  |
-                          Decidability and Complexity Analysis
-:00-18:30 Management Committee meeting (for COST only)
-</code>
 === Monday, 21 January 2013 ===
-<code>
+| 9:00-10:00 | Invited Talk: **Francesco Ranzato - Complete Abstractions Everywhere** (shared with VMCAI) |
-:00-10:00 VMCAI Invited Talk: Francesco Ranzato - Complete Abstractions Everywhere
+^ 10:00-10:30 ^ Break ^
-:00-10:30 Break
+| 10:30-11:00 | Mnacho Echenim: On an abductive approach to error detection |
-: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 |
-: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 |
-:30-12:00 Mark Micallef: The Equivalent Mutant Problem in Mutation Testing
+^ 12:00-14:00 ^ Lunch ^
-:00-14:00 Lunch
+| 14:00-15:00 | Invited Talk: **Joe Leslie-Hurd - Theory Engineering Using Composable Packages** (shared with VMCAI) |
-:00-15:00 Invited Talk: Joe Leslie-Hurd - Theory Engineering Using Composable Packages
+| 15:00-15:30 | Markus Rabe: A logic for hyperproperties |
-:00-15:30 Markus Rabe: A logic for hyperproperties
+| 15:30-16:00 | Hossein Hojjat: Combining Infinite-state Verification Techniques in Analyzing Integer Models |
-:30-16:00 Hossein Hojjat: Combining Infinite-state Verification Techniques in Analyzing Integer Models
+^ 16:00-16:15 ^ Break ^
-:00-16:15 Break
+| 16:15-16:45 | Pavle Subotic: Automatic Compositional Analysis of Timed Automata |
-: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 |
-: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 |
-:15-17:45 Daniel Larraz: Proving termination of C-like programs using MAX-SMT
+^ 17:45-18:00 ^ Break ^
-:45-18:00 Break
+| 18:00-19:00 | Invited Talk: **Ken McMillan - Logic as the lingua franca of software verification** (shared with VMCAI) |
-:00-19:00 Invited Speaker: Ken McMillan - Logic as the lingua franca of software verification
-</code>
 ===== General Information =====
@@ Line 47: / 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/
-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 =====
@@ Line 56: / Line 55: @@
 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//