|
|
Formal Methods
| Head : I. Walukiewicz |  |
Research themes :
The Formal Methods team is active in many areas of theoretical computer science and its applications. Its work is grouped in three themes:
- Infrmatique Linguistique (IL)
- Head: C. Retoré.
- Keywords: Informatics and linguistics, automatic language processing, formal grammars, resource logic, linear logic, Lambek calculus, Lambda calculus.
- Logiques, Graphes et Langages (LGL)
- Head: B. Courcelle.
- Keywords: Graph decomposition, recognisability, monadic second order logic, mu calculus, games, proof assistants, finite description of countable objects.
- Modélisation et Vérification (MV)
- Head: I. Walukiewicz.
- Keywords: Verification, synthesis, infinite state systems, concurent systems, real-time, program logics, symbolic representations.
Rapport d'activité (in French) (PDF)
----
Events:
- ESSLLI'09 21st European Summer School in Logic, Language and Information, July 2009).
- STACS'08, Symposium on Theoretical Aspects of Computer Science, (February 2008).
- AltaRICA'07, wokshop of AltaRICA users and developers. (November 2007).
- MOVEP'06, MOdelling and VErifying parallel Processes (June 2006).
Software:
- AltaRica: language and tools for modelling and verification.
- Autowrite: a tool for checking properties of term rewrite systems.
- FASTer: a tool dedicated to the analysis of infinite systems.
- Grail: a tool for the development and prototyping of grammar fragments for categorial logics.
- ViSiDiA: Visualization and Simulation of Distributed Algorithms.
- XFLG: Implantation d’un analyseur pour grammaire LFG.
Projects:
- CRYSCOE (Cryptography for the Security of Embedded Codes), ANR "Sécurité des systèmes embarqués et Intelligence Ambiante", 2005-2008.
- Timed-DISCOVERI (Timed and distributed models for control and verification), Indo-French Research network Project, 2005-2008.
- A3PAT (Automatic Assistance for Proof Assistants with Traces), ANR, "Sécurité et Informatique" 2006-2009.
- GRAAL (Decompositions of Graphs and Algorithms), ANR "programme blanc", 2006-2009.
- MOSAIQUE (High Level Syntactic Models), ARC INRIA, 2006-2007.
- AVeriSS (Automated Verification of Software Systems), ANR "Sécurité et Informatique", 2007-2010.
- DocFlow (Analysis, monitoring and optimisation of Web documents and services), ANR "Masse de Données et Connaissances Ambiantes" 2007-2009.
- DOTS (Distributed Open and Timed Systems), ANR "Sécurité et Informatique" 2007--2010.
- PRELUDE (Towards a Theoretical Pragmatics Based on Games and Continuations), ANR, "programme blanc", 2007-2010.
- SPaCIFY (Engineering of Integrated Models and Formal Methods for Spaceflight Software Development), ANR "Technologies logicielles", 2007-2009.
- RIMEL (Incremental Refinement of Event Models), ANR "Sécurité et Informatique", 2007-2009.
- GAMES (Games for Design and Verification) ESF Research Networking Programme, 2008-2012.
- BINCOA (Symbolic Methods for BINary Code Analysis), ANR ARPEGE, 2009-2011.
- GDR IM Informatics and Mathematics.
- GDR GPL Software and Program Engineering.
Seminars:
|
|