This is an old revision of the document!


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

{{:cost-logo.png|COST LOGO}} ====== 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. * **[[synthesis|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 [[http://software.imdea.org/~cesar/|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) * [[http://nts.imag.fr/index.php/Main_Page | Numerical Transition Systems]] ===== 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 * **[[http://argo.matf.bg.ac.rs/events/2010/fatpa2010/fatpa2010.html|Belgrade 2010]]**, January 29-30th with 3rd FATPA Workshop (organization: **Predrag Janicic**) * **[[SVARM10|SVARM 2010]]** in Edinburgh, at [[http://www.floc-conference.org/|FLOC 2010]], July 20-21 (organization: **Paul Jackson**) * **[[Lugano|Lugano 2010]]**, October 18-19, with [[http://fmcad10.iaik.tugraz.at/|FMCAD 2010]] and AVM (organization: **Viktor Kuncak** and **Natasha Sharygina**) * **[[svarm11|SVARM 2011]]** meeting, 1-3 April 2011, Saarbruecken, with [[http://www.etaps.org/|ETAPS]] (organization: **Bernd Finkbeiner** and **Rupak Majumdar**) [[https://picasaweb.google.com/barbara.jobstmann/SVARM?authuser=0&authkey=Gv1sRgCNqsmMmuhZubjAE&feat=directlink|Pictures]] [[https://picasaweb.google.com/barbara.jobstmann/ETAPS?authuser=0&authkey=Gv1sRgCNjWlPfGhti-zwE&feat=directlink|Pictures of social event]] * [[http://www.cs.berkeley.edu/~bodik/dagstuhl-2011.html|Summer School on Synthesis]] ([[http://www.dagstuhl.de/en/program/calendar/evhp/?semnr=11322|Dagstuhl page]]), 07-12 August 2011, Dagstuhl Schloss, Germany * **[[https://sites.google.com/site/torino2011ic0901/|Turin 2011]]** meeting, Oct 3-4, 2011, Turin, co-located with [[http://foveoos2011.cost-ic0701.org/|International Conference on Formal Verification of Object-Oriented Software]] and [[http://fmco.liacs.nl/|International Symposia on Formal Methods for Components and Objects]] (organization: **Alessandro Armando**, **Maria Paola Bonacina**, and **Luca Paolini**) [[https://picasaweb.google.com/barbara.jobstmann/20111003_Torino?authuser=0&authkey=Gv1sRgCOupzY2Mua3AVA&feat=directlink|Pictures]] * **[[Tallinn12|Tallinn 2012]]** meeting collocated with **[[http://www.etaps.org/|ETAPS]] 2012** and organized by **[[http://users.ics.tkk.fi/kepa/|Keijo Heljanko]]** and **[[http://yquem.inria.fr/~herbelin/|Hugo Herbelin]]** * **[[Manchester12|Manchester 2012]]** in collaboration with the VERIFY workshop, collocated with [[http://ijcar.cs.manchester.ac.uk/|IJCAR 2012]] and part of the [[http://www.mathcomp.leeds.ac.uk/turing2012/|2012 Alan Turing year]] celebration * **[[Haifa12|Haifa 2012]]** meeting organized by **Eran Yahav** and **Armin Biere** * **[[Rome13|Rome 2013]]** meeting organized by **Maria Paola Bonacina** and **Cesar Sanchez** * **[[Malta13|Malta 2013]]** meeting organized by **Gordon Pace** and **Cesar Sanchez** * {{:new.png?60|new}} **[[Madrid13|Madrid 2013]]** final meeting ===== Related Competitions ===== * [[http://www.smtcomp.org/|SMT-COMP]] - SMT Solver Competition * [[http://www.cs.miami.edu/~tptp/CASC/|CASC]] - CADE ATP System Competition * [[http://www.termination-portal.org/wiki/Termination_Competition|Termination Competition]] - Proving Termination of Programs and Rewrite Systems * [[http://fmv.jku.at/hwmcc10/|HWMCC]] - Hardware Model Checking Competition * [[http://nts.imag.fr/index.php/Main_Page|NTS-COMP]] - Numerical Transition Systems Competition Other competitions: * [[http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/NSV3/|NSV]] * [[http://mcc.lip6.fr/|Model Checking Contest @ PETRI NETS]] * [[http://sv-comp.sosy-lab.org/|Competition on Software Verification]] * [[http://foveoos2011.cost-ic0701.org/verification-competition|Interactive Verification Competition at FOVEOOS 2012]] * [[https://sites.google.com/site/vstte2012/compet|Competition at VSTTE 2012]] ===== 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 [[:internal:stsm-guide|Guide to Application Process for IC0901 Members]] ===== COST Action IC0901 ===== {{:cost-logo.png|COST}} Action IC0901: Rich-Model Toolkit - An Infrastructure for Reliable Computer Systems ^ [[internal:top|For Internal Page Click Here]] ^ Official pages: * [[http://w3.cost.eu/index.php?id=177&action_number=IC0901|Current MC Members]] (as recorded by COST) * [[http://cost.eu/typo3conf/ext/bzb_securelink/pushFile.php?cuid=253&file=fileadmin/domain_files/ICT/Action_IC0901/mou/IC0901-e.pdf|Memorandum with Proposed Action Activities]] ({{:ic0901-e.pdf|Local PDF}}) About COST: http://www.cost.eu/ ===== Mailing Lists ===== ((This site and the mailing lists are hosted by the [[http://www.epfl.ch/index.en.html|Swiss Federal Institute of Technology, Lausanne (EPFL)]] and managed by the [[http://lara.epfl.ch|LARA group]])) 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 ===== The following is a partial list of experts with interest in the initiative: * [[http://www.ai-lab.it/armando/|Alessandro Armando]] (Italy) * [[http://formal.iti.kit.edu/english/team_beckert.php|Bernhard Beckert]] (Germany) * [[http://research.microsoft.com/en-us/people/jjb/default.aspx|Josh Berdine]] (UK) * [[http://www.ii.uib.no/~bezem/|Marc Bezem]] (NO) * [[http://www.itu.dk/~birkedal/|Lars Birkedal]] (Denmark) * [[http://www.ist.tugraz.at/staff/bloem/|Roderick Bloem]] (Austria) - **Vice Chair** * [[http://fmv.jku.at/biere/|Armin Biere]] (Austria) {{:slides:biere-fmv.pdf|intro}} - Vice Chair of Work Group 2 on Decision Procedures * [[http://profs.sci.univr.it/~bonacina/|Maria Paola Bonacina]] (Italy) {{:slides:introunivr.pdf|intro}} - Chair of Work Group 2 on Decision Procedures * [[http://cui.unige.ch/~buchs/Site/About_Me.html|Didier Buchs]] (Switzerland) * [[http://www.comlab.ox.ac.uk/people/radu.calinescu/|Radu Calinescu]] (United Kingdom) * [[http://www.lsi.upc.edu/~erodri/|Enric Rodríguez Carbonell]] (Spain) {{:slides:rodriguezintro.pdf|intro}} * [[http://www.ist.ac.at/chatterjee-group/team/dr-krishnendu-chatterjee/|Krishnendu Chatterjee]] (Austria) * [[https://es.fbk.eu/people/cimatti/|Alessandro Cimatti]] (Italy) * Samuel Dellacherie, Aerielogic (France) * [[http://www.lsv.ens-cachan.fr/~doyen/|Laurent Doyen]] (France) * [[http://domino.research.ibm.com/comm/research_people.nsf/pages/eisner.index.html|Cindy Eisner]] (Israel) * [[http://react.cs.uni-sb.de/finkbeiner|Bernd Finkbeiner]] (Germany) * [[http://imft.ftn.uns.ac.rs/~silvia/|Silvia Ghilezan]] (Serbia) {{:slides:ghilezan-uns-description.pdf|intro}} * [[http://www.cse.chalmers.se/~reiner/|Reiner Haehnle]] (Sweden) {{:slides:gothenburg-cth-presentation-rmt.pdf|intro}} * [[http://www.tcs.hut.fi/~kepa/|Keijo Heljanko]], Vice Chair of Work Group 3 on the Analysis of Executable Models * [[http://pauillac.inria.fr/~herbelin/index-eng.html|Hugo Herbelin]] (France) * [[http://web.comlab.ox.ac.uk/people/Ian.Horrocks/|Ian Horrocks]] (UK) * [[http://www.penjili.org/|Charles Hymans, EADS IW]] (France) * [[http://www-verimag.imag.fr/~iosif/|Radu Iosif]] (France) * [[http://gabrielistrate.weebly.com/|Gabriel Istrate]] * [[http://homepages.inf.ed.ac.uk/pbj/|Paul Jackson]] (UK) - Vice Chair of Work Group 1 on Rich Model Language * [[http://www.matf.bg.ac.rs/~janicic/|Predrag Janicic]] (Serbia) {{:slides:argogrouppresentation.pdf|intro}} * [[http://www-verimag.imag.fr/~jobstman/|Barbara Jobstmann]] (France) - Chair of Work Group 4 on Synthesis * [[http://www.zurich.ibm.com/~hvo/|Hagen Völzer]] (Switzerland) * [[http://www.chalmers.se/cse/EN/people/claessen-koen|Koen Claessen]] (Sweden) * [[http://www.kroening.com/|Daniel Kröning]] (UK) * [[http://lara.epfl.ch/~kuncak/|Viktor Kuncak]] (Switzerland) * [[http://www.cs.utt.ro/~marius/|Marius Minea]] (Romania) * [[http://www.tcs.hut.fi/~ini/|Ilkka Niemelä]] (Finland) * [[http://www4.informatik.tu-muenchen.de/~nipkow/|Tobias Nipkow]] (Germany) - Chair of Work Group 1 on Rich Model Language * [[http://www.ii.uni.wroc.pl/~pacholsk/index.phtml?lang=en|Leszek Pacholski]], Poland * [[http://www.cs.ucla.edu/~rupak/|Rupak Majumdar]], Germany * [[http://www.cs.um.edu.mt/gordon.pace/|Gordon Pace]], Malta * [[http://www.di.unito.it/~paolini/|Luca Paolini]], Italy * [[http://users.abo.fi/iporres/|Ivan Porres]], Finland * [[http://www.cl.cam.ac.uk/~lp15/|Lawrence C. Paulson]], UK (WG Member) * [[http://www.cs.tau.ac.il/~rabinoa/|Alexander Rabinovich]] (Israel) * [[http://www.loria.fr/~ranise/|Silvio Ranise]] (France/Italy) * [[http://www.ulb.ac.be/di/ssd/jfr/|Jean-Francois Raskin]] (Belgium) * [[http://www.cs.cas.cz/~ratschan/|Stefan Ratschan]] (Czech Republic), interests: solving non-linear numerical constraints, hybrid systems * [[http://www.philipp.ruemmer.org/|Philipp Ruemmer]] (Sweden) * [[http://www.mpi-sws.mpg.de/~rybal/|Andrey Rybalchenko]] (Germany) * [[http://theory.stanford.edu/~cesar|Cesar Sanchez]] (Spain) - **Chair and Grant Holder** * [[http://www.csl.sri.com/users/shankar/|Natarajan Shankar]] (US) * [[http://www.imada.sdu.dk/~petersk/|Peter Schneider-Kamp]] (Denmark) [[http://ditwww.epfl.ch/cgi-perl/EPFLTV/home.pl/?page=video&lang=2&connected=0&id=650&plugin=9&checkplugin=1|Talk Video]] * [[http://www.inf.unisi.ch/faculty/sharygina/|Natasha Sharygina]] (Switzerland) {{:slides:sharygina_group.pdf|intro}} - Chair of Work Group 3 on the Analysis of Executable Models * [[http://www.itu.dk/~sestoft/|Peter Sestoft]] (Denmark) * [[http://www.fri.uni-lj.si/en/personnel/5594/oseba.html|Iztok Starc]] (Slovenia) * [[http://www.cs.uiowa.edu/~astump/|Aaron Stump]] (US) * [[http://www.cs.miami.edu/~geoff/|Geoff Sutcliffe]] (US) * [[http://www.cs.uiowa.edu/~tinelli/|Cesare Tinelli]] (US) * [[http://www.liafa.jussieu.fr/~touili/|Tayssir Touili]] (France) * [[http://www.fri.uni-lj.si/en/personnel/1121/oseba.html|Denis Trcek]] (Slovenia) * [[http://www.cs.purdue.edu/homes/jv/|Jan Vitek]] (US) * [[http://www.fit.vutbr.cz/~vojnar/|Tomas Vojnar]] (Czech Republic) * [[http://www.cs.technion.ac.il/people/yahave/|Eran Yahav]], Technion, Israel