Differences
This shows you the differences between two versions of the page.
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/15 16:03] 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 ====== |
+ | |||
+ | ===== PROGRAM ===== | ||
+ | |||
+ | === Sunday, 20 January 2013 === | ||
+ | |||
+ | | 9:00-10:00 | (VMCAI) Invited Talk: **Leonardo de Moura - A Model-Constructing Satisfiability Calculus** | | ||
+ | ^ 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 | (VMCAI) Invited Talk: **Eran Yahav - Abstraction-Guided Synthesis** | | ||
+ | | 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 | (COST Only) Management Committee meeting | | ||
+ | |||
+ | === Monday, 21 January 2013 === | ||
+ | |||
+ | | 9:00-10:00 | VMCAI Invited Talk: **Francesco Ranzato - Complete Abstractions Everywhere** | | ||
+ | ^ 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** | | ||
+ | | 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 Speaker: **Ken McMillan - Logic as the lingua franca of software verification** | | ||
+ | |||
+ | ===== 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 6: | Line 43: | ||
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, 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 ===== |