Rich-Model Toolkit

About the Initiative

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

A Sample of 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 highlevel specifications. Extending decision procedures to perform synthesis tasks. Connections between invariant generation and code synthesis.

Meetings

Past meetings:

Kick-off meeting in Brussels, October 30th, 2009
Belgrade, WG1+2 Meeting, January 29-30th with the 3rd Workshop on Formal and Automated Theorem Proving with Applications
- Local organization: Predrag Janicic

Upcoming Meetings:

SVARM at FLOC 2010, July 20-21, 2010
- Local organization: Paul Jackson
Lugano, WG2+3 Meeting, with FMCAD 2010, October 18-19, 2010, with Alpine Verification Meeting
- Local organization: Viktor Kuncak and Natasha Sharygina

COST Action IC0901

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

For Internal Page Click Here

Official pages:

About COST: http://www.cost.esf.org/

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:

http://laraserver.epfl.ch/wws

Experts

From countries participating under the COST European Cooperation:

Alessandro Armando (Italy)
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
Enric Rodríguez Carbonell (Spain) intro
Samuel Dellacherie, Aerielogic (France)
Silvia Ghilezan (Serbia) intro
Reiner Haehnle (Sweden) intro
Keijo Heljanko
Ian Horrocks (UK)
Gabriel Istrate
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)
Viktor Kuncak (Switzerland) - Chair, Grant Holder
Marius Minea (Romania)
Ilkka Niemelä (Finland)
Tobias Nipkow (Germany) - Chair of Work Group 1 on Rich Model Language
Leszek Pacholski, Poland
Rupak Majumdar, Germany
Ivan Pores, Finland
Alexander Rabinovich (Israel)
Stefan Ratschan (Czech Republic), interests: solving non-linear numerical constraints, hybrid systems
Philipp Ruemmer (UK)
Andrey Rybalchenko (Germany)
Cesar Sanchez (Spain)
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)
Tayssir Touili (France)
Denis Trcek (Slovenia)
Tomas Vojnar (Czech Republic)
Eran Yahav, Technion, Israel

Additional experts: