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 [2012/10/16 10:57]
vkuncak
rome13 [2013/01/18 15:54]
vkuncak
Line 1: Line 1:
-====== Rich Model Toolkit (COST Action IC0901) Meeting: Rome 2013 ======+====== ​Workshop on Synthesis, Verification and Analysis of Rich Models: Rome, 20-21 January ​2013 ======
  
-Meeting collocated with [[http://popl.mpi-sws.org/2013/|POPL 2013]], organized by **Maria Paola Bonacina** and **Cesar Sanchez**.+Location: ​[[http://www.robertonaldicollection.com/eng/parco_dei_principi/​hotel_luxury_rome_parioli.htm|Hotel Parco Dei Principi]], Via GFrescobaldi,​ 5 - 00198 Rome, Italy, [[http://​popl13.di.univr.it/​styled-10/​styled-9/​files/​download-the-map.pdf|Room Sforza A]]
  
-Information about the Action: ​http://richmodels.epfl.ch/+([[http://popl13.di.univr.it/index.html|Omniae viae ferunt Romam]] and so do many flights.)
  
-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.+===== PROGRAM =====
  
-==== Scope of the Event ====+=== 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**. 
 + 
 +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, 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 ===== 
 + 
 +We are pleased to confirm keynotes from: 
 +  * **[[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//​ 
 + 
 +===== Scope of the Event =====
  
 Researchers have developed a number of useful tools for automated analysis of particular classes of models of computer Researchers have developed a number of useful tools for automated analysis of particular classes of models of computer
Line 22: Line 73:
 without formal assurance guarantees. without formal assurance guarantees.
  
-==== Example topics of interest ====+===== Example topics of interest ​=====
  
   * **Standardization of expressive languages.** Formats to represent systems, formulas, proofs, counterexamples. Translation between specification languages. Benchmarks and competitions for automated reasoning, verification,​ analysis, synthesis.   * **Standardization of expressive languages.** Formats to represent systems, formulas, proofs, counterexamples. Translation between specification languages. Benchmarks and competitions for automated reasoning, verification,​ analysis, synthesis.