Differences

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

--- rome13 [2012/09/23 17:35]
vkuncak created
+++ rome13 [2013/01/15 15:57]
vkuncak
@@ Line 1: / Line 1: @@
-====== 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 | Management Committee meeting (for COST only) |
+=== Monday, 21 January 2013 ===
+<code>
+:00-10:00 VMCAI Invited Talk: Francesco Ranzato - Complete Abstractions Everywhere
+:00-10:30 Break
+:30-11:00 Mnacho Echenim: On an abductive approach to error detection
+:00-11:30 Hannes Mehnert: Unified Development and Verification of Java Programs in Eclipse
+:30-12:00 Mark Micallef: The Equivalent Mutant Problem in Mutation Testing
+:00-14:00 Lunch
+:00-15:00 Invited Talk: Joe Leslie-Hurd - Theory Engineering Using Composable Packages
+:00-15:30 Markus Rabe: A logic for hyperproperties
+:30-16:00 Hossein Hojjat: Combining Infinite-state Verification Techniques in Analyzing Integer Models
+:00-16:15 Break
+:15-16:45 Pavle Subotic: Automatic Compositional Analysis of Timed Automata
+:45-17:15 Predrag Janicic: Automated Generation of Formal and Readable Proofs of Mathematical Theorems
+:15-17:45 Daniel Larraz: Proving termination of C-like programs using MAX-SMT
+:45-18:00 Break
+:00-19:00 Invited Speaker: Ken McMillan - Logic as the lingua franca of software verification
+</code>
+===== 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, 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)
+  * **[[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
+systems:
+  * software vendors are using static analyses supported by automated theorem provers and constraint solvers to prevent software crashes;
+  * hardware manufacturers are using SAT solvers,model checkers, and theorem provers to identify and correct errors that could have enormous financial consequences;
+  * description logic reasoners analyze relationships between tens of thousands of terms in medical ontologies and verify their consistency;
+  * aircraft manufacturers and space agencies are using analysis tools based on abstract interpretation to eliminate errors in aircraft control software.
+Despite these successes, today’s automated analysis methods are not widespread in engineering practice.
+Among the factors contributing to this state of affairs are the limitations of the tools themselves:
+insufficient automation, specialized input formats, and no support for high-level synthesis. Another factor is the lack of standards
+of quality that would easy tool interoperability and give formally certified computer system a competitive advantage over systems
+without formal assurance guarantees.
+===== 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.
+  * **Decision procedures:** Decision procedures for new classes of constraints. SAT and SMT implementation and certification. Encoding synthesis and analysis problems into SMT. Description logics and scalable reasoning about knowledge bases.
+  * **Transition system analysis:** Abstraction-based approaches and refinement for verification of infinite-state systems. Constraint-based program analysis. Data-flow analysis for complex domains. Extracting transition systems from programming languages and bytecodes.
+  * **High-level synthesis:** New algorithms for synthesis from high-level specifications. Extending decision procedures to perform synthesis tasks. Connections  between invariant generation and code synthesis.
-Meeting collocated with [[http://popl.mpi-sws.org/2013/|POPL 2013]].