Rich-Model Toolkit
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
- Verification Modulo Theories (more information available soon)
Meetings
The scientific program of our meetings is open to public and runs under the SVARM workshop series. Our meetings include the following:
- Brussels 2009: Organizational Kick-Off Meeting on 30 October 2009
- Belgrade 2010, January 29-30th with 3rd FATPA Workshop (organization: Predrag Janicic)
- SVARM 2010 in Edinburgh, at FLOC 2010, July 20-21 (organization: Paul Jackson)
- Lugano 2010, October 18-19, with FMCAD 2010 and AVM (organization: Viktor Kuncak and Natasha Sharygina)
- SVARM 2011 meeting, 1-3 April 2011, Saarbruecken, with ETAPS (organization: Bernd Finkbeiner and Rupak Majumdar) Pictures Pictures of social event
- Summer School on Synthesis (Dagstuhl page), 07-12 August 2011, Dagstuhl Schloss, Germany
- Turin 2011 meeting, Oct 3-4, 2011, Turin, co-located with International Conference on Formal Verification of Object-Oriented Software and International Symposia on Formal Methods for Components and Objects (organization: Alessandro Armando, Maria Paola Bonacina, and Luca Paolini) Pictures
- Manchester 2012 in collaboration with the VERIFY workshop, collocated with IJCAR 2012 and part of the 2012 Alan Turing year celebration
- Haifa 2012 meeting organized by Eran Yahav and Armin Biere
- Rome 2013 meeting organized by Maria Paola Bonacina and Cesar Sanchez
- Malta 2013 meeting organized by Gordon Pace and Cesar Sanchez
- Madrid 2013 October, 17-18, 2013. Final meeting.
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
COST Action IC0901
Action IC0901: Rich-Model Toolkit - An Infrastructure for Reliable Computer Systems
Official pages:
- Current MC Members (as recorded by COST)
About COST: http://www.cost.eu/
Mailing Lists
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:
- Alessandro Armando (Italy)
- Bernhard Beckert (Germany)
- Josh Berdine (UK)
- Marc Bezem (NO)
- Lars Birkedal (Denmark)
- Roderick Bloem (Austria) - Vice Chair
- Armin Biere (Austria) intro - Vice Chair of Work Group 2 on Decision Procedures
- Maria Paola Bonacina (Italy) intro - Chair of Work Group 2 on Decision Procedures
- Didier Buchs (Switzerland)
- Radu Calinescu (United Kingdom)
- Enric Rodríguez Carbonell (Spain) intro
- Krishnendu Chatterjee (Austria)
- Alessandro Cimatti (Italy)
- Samuel Dellacherie, Aerielogic (France)
- Laurent Doyen (France)
- Cindy Eisner (Israel)
- Bernd Finkbeiner (Germany)
- Silvia Ghilezan (Serbia) intro
- Reiner Haehnle (Sweden) intro
- Keijo Heljanko, Vice Chair of Work Group 3 on the Analysis of Executable Models
- Hugo Herbelin (France)
- Ian Horrocks (UK)
- Charles Hymans, EADS IW (France)
- Radu Iosif (France)
- Paul Jackson (UK) - Vice Chair of Work Group 1 on Rich Model Language
- Predrag Janicic (Serbia) intro
- Barbara Jobstmann (France) - Chair of Work Group 4 on Synthesis
- Hagen Völzer (Switzerland)
- Koen Claessen (Sweden)
- Daniel Kröning (UK)
- Viktor Kuncak (Switzerland)
- Marius Minea (Romania)
- Ilkka Niemelä (Finland)
- Tobias Nipkow (Germany) - Chair of Work Group 1 on Rich Model Language
- Leszek Pacholski, Poland
- Rupak Majumdar, Germany
- Gordon Pace, Malta
- Luca Paolini, Italy
- Ivan Porres, Finland
- Lawrence C. Paulson, UK (WG Member)
- Alexander Rabinovich (Israel)
- Silvio Ranise (France/Italy)
- Jean-Francois Raskin (Belgium)
- Stefan Ratschan (Czech Republic), interests: solving non-linear numerical constraints, hybrid systems
- Philipp Ruemmer (Sweden)
- Andrey Rybalchenko (Germany)
- Cesar Sanchez (Spain) - Chair and Grant Holder
- Natarajan Shankar (US)
- Peter Schneider-Kamp (Denmark) Talk Video
- Natasha Sharygina (Switzerland) intro - Chair of Work Group 3 on the Analysis of Executable Models
- Peter Sestoft (Denmark)
- Iztok Starc (Slovenia)
- Aaron Stump (US)
- Geoff Sutcliffe (US)
- Cesare Tinelli (US)
- Tayssir Touili (France)
- Denis Trcek (Slovenia)
- Jan Vitek (US)
- Tomas Vojnar (Czech Republic)
- Eran Yahav, Technion, Israel