COST LOGO

Rich-Model Toolkit

NEWS: Acta Informatica Special Issue

About the Initiative

This rich model toolkit initiative 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. It includes participants from over 20 countries, over 50 research groups. The unifying idea of rich models is to explore precise mathematical and formal models of key aspects of our infrastructure, developing algorithms, tools, and common standardized formats. Through our networking activities we aim to establish connections between different tools, methodologies, and communities.

Selected 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.

The chair and the grant holder of the action is Cesar Sanchez.

The Action holds general meetings typically twice a year, with one of these meetings publicized as the SVARM workshop.

Recent Activities

Meetings

The scientific program of our meetings is open to public and runs under the SVARM workshop series. Our meetings include the following:

Related Competitions

  • SMT-COMP - SMT Solver Competition
  • CASC - CADE ATP System Competition
  • Termination Competition - Proving Termination of Programs and Rewrite Systems
  • HWMCC - Hardware Model Checking Competition
  • NTS-COMP - Numerical Transition Systems Competition

Other competitions:

Short-Term Scientific Missions

Short-Term Scientific Missions in 2010:

  • Dr Florian Haftmann
  • Mr Florian Lonsing
  • Dr Philipp Ruemmer
  • Mr Alejandro Sanchez
  • Dr Filip Maric

Short-Term Scientific Missions in 2011:

  • Dr Enric Rodriguez-Carbonell
  • Dr Tayssir Touili
  • Mr Siert Wieringa
  • Mr Yaron Velner
  • Dr Swen Jacobs
  • Dr César Sánchez

Short-Term Scientific Missions in 2012:

  • Ms Svetlana Jaksic
  • Mr Ronald Toegl
  • Mr Markus Rabe
  • Dr Corneliu Popeea
  • Mr Simone Fulvio Rollini
  • Dr Michael Tautschnig
  • Mr Michał Skrzypczak
  • Mr Hossein Hojjat

Short-Term Scientific Missions in 2013:

  • Dr Ondrej Sery
  • Mr Pavel Jancik
  • Ondrej Lengal
  • Andrijana Stamenkovic

Guide to Application Process for IC0901 Members

COST Action IC0901

COST

Action IC0901: Rich-Model Toolkit - An Infrastructure for Reliable Computer Systems

For Internal Page Click Here

Official pages:

About COST: http://www.cost.eu/

Mailing Lists

1)

Rich Model Toolkit Mailing List (for broad technical discussions):

  • richmodels-all

Management Committee Mailing List (for decision making and Action logistics):

  • richmodels-mc

Both lists have domain epfl.ch

URL for configuration and archive:

Experts

The following is a partial list of experts with interest in the initiative:

1) This site and the mailing lists are hosted by the Swiss Federal Institute of Technology, Lausanne (EPFL) and managed by the LARA group