Synthesis, Verification, and Analysis of Rich Models (SVARM) 2010

SVARM Program

Registration is through FLoC Registation

Synthesis, Verification, and Analysis of Rich Models (SVARM) will take place July 20-21 in Edinburgh, UK as part of FLoC 2010. The event is affiliated with two FLoC conferences:

The event will be simultaneously a meeting for all work groups of the Rich Model Toolkit Initiative (http://richmodels.org)

The event explores directions and techniques for making automated reasoning (including analysis and synthesis) applicable to a wider range of problems, as well as making them easier to use by researchers, software developers, hardware designers, and information system users and developers.

Invited Talks:

SVARM Program

Abstract submission is now closed (Call for Abstracts in Text Format)

Scope of the Event

Researchers have recently 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.

Program Committee

  • Roderick Bloem (TU Graz, Austria)
  • Armin Biere (Johannes Kepler University, Linz, Austria)
  • Maria Paola Bonacina (Università degli Studi di Verona, Italy)
  • Enric Rodriguez Carbonell (TU Catalonia, Spain)
  • Silvia Ghilezan (University of Novi Sad, Serbia)
  • Ian Horrocks (University of Oxford, UK)
  • Paul Jackson (University of Edinburgh, UK)
  • Predrag Janičić (University of Belgrade, Serbia)
  • Viktor Kuncak (EPFL, Switzerland)
  • Marius Minea (Politehnica University of Timisoara, Romania)
  • Ilkka Niemelä (Helsinki University of Technology, Finland)
  • Tobias Nipkow (TU Munich, Germany)
  • Alexander Rabinovich (Tel-Aviv University, Israel)
  • Stefan Ratschan (Academy of Sciences, Czech Republic)
  • Andrey Rybalchenko (MPI-SWS, Germany)
  • Cesar Sanchez (IMDEA-Software, Spain)
  • Natasha Sharygina (University of Lugano, Switzerland)
  • Tomáš Vojnar (Brno Univ. of Technology, Czech Republic)

Program and Conference Chairs

Local organization: Paul Jackson

Description of the COST Action IC0901

Important dates:

  • April 23: Abstract Submission Deadline (CLOSED)
  • April 30: Notification. Program Published Online
  • July 20-21: camera-ready version of talks to be presented to the audience :)

The focus of the event is on presentations and discussions; there will be neither electronic nor paper proceedings before the event.

SVARM Program