This is an old revision of the document!


A PCRE internal error occured. This might be caused by a faulty plugin

====== 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) | </code> === Monday, 21 January 2013 === <code> 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 </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.