Méthodes Formelles
Responsable : J. LerouxMembres Publications




Thèmes de recherche :

L'équipe "Méthodes Formelles" est active dans plusieurs domaines de l'informatique fondamentale et de ses applications. Ses travaux sont regroupés en deux thèmes:

  • Logiques, graphes et langages (LGL)
    • Responsable : S. Lombardy.
    • Mots clés : Décompositions de graphes, reconnaissabilité, logique du second-ordre monadique, mu-calcul, lambda-calcul, jeux, assistants de preuves, descriptions finies d'objets dénombrables.
  • Modélisation et vérification (MV)
    • Responsable : L. Simon.
    • Mots clés : Vérification, synthèse, systèmes infinis, systèmes concurrents, systèmes temps-réel, formalismes avec données, calcul symbolique, analyse de code binaire.



Rapport d'activité 2009-2014 (PDF)




Événements :

  • JFPC'15 (Journées Francophones de Programmation par Contraintes), 22-24 juin 2015.
  • ALFA'15 (Automata, logic, formal languages and algebra), 15-17 juin 2015.
  • RP'12, 6th International workshop on Reachability Problems, 17-19 septembre 2012.
  • Workshop Bruno Courcelle, 18-20 juin 2012.
  • EPIT'11, Ecole de printemps d'Informatique Théorique 2011. Carcans-Maubuisson, 23-27 mai 2011.
  • LCS'10, workshop "Logic, categories, semantics", novembre 2010.
  • ESSLLI'09 21st European Summer School in Logic, Language and Information, juillet 2009.
  • STACS'08, Symposium on Theoretical Aspects of Computer Science, février 2008.
  • AltaRICA'07, workshop of AltaRICA users and developers, novembre 2007.
  • MOVEP'06, MOdelling and VErifying parallel Processes, juin 2006.


Logiciels :

  • Acme++: tool which computes stabilization monoids in order to solve three algorithmic problems: Computing the star-height of a regular language, deciding boundedness and equivalence for regular cost functions and deciding whether a leaktight probabilistic automaton has value 1.
  • AltaRica: language and tools for modeling and verification.
  • Autograph: tool for verifying properties of graphs of bounded clique-width.
  • FASTer: tool for the analysis of infinite systems.
  • Glucose: SAT-solver.
  • Grail: tool for the development and prototyping of grammar fragments for categorial logics.
  • Insight: tool for binary program analysis framework.
  • TChecker: tool for analysis of timed systems.
  • ViSiDiA: Visualization and Simulation of Distributed Algorithms.


Projets :

  • ANR Stoch-MC (Modèles stochastiques: passage à l’échelle pour le Model Checking), ANR Blanc, 2014-2018.
  • ANR ExStream (Extensions de l'évaluation par flux,) ANR JCJC, 2014-2018.
  • Impex (Intégration des sémantiques implicite et explicite dans les développements de systèmes discrets fondés sur la preuve), ANR INS, 2013-2017.
  • Synthesis of Stream Processors (O. Gauwin), PEPS CNRS, 2013-2015.
  • INEDIT (Interactivité dans l'écriture du temps), ANR CONTINT, 2012-2015.
  • POLYMNIE (Analyse et synthèse dans les grammaires catégorielles abstraites : du lexique au discours), ANR CONTINT, 2012-2015.
  • LOCI (Locativité et interactivité en logique, linguistique et informatique théorique), ANR BLANC, 2010-2014.
  • SAFE (Safe Automotive soFtware architEcture), projet UE, 2011--2014.
  • VACSIM (Validation de la commande des systèmes critiques par couplage simulation et méthodes d'analyse formelle), ANR INS 2011-2015.
  • MARSHAL, projet FUI (Fonds Unique Interministériel), 2012-2014.
  • REACHARD (Taming Hard Reachability Problems for Counter Systems), ANR BLANC (SIMI 2), 2011-2014.
  • FREC (Frontiers of recognizability), ANR BLANC, 2010-2014.
  • Stochastic Games for Verification (H. Gimbert), PEPS 2011 - 2013.
  • GAMES (Games for Design and Verification) ESF Research Networking Programme, 2008-2012.
  • BINCOA (Symbolic Methods for BINary Code Analysis), ANR ARPEGE, 2009-2012.
  • ENUM, ANR 2007-2011.
  • AVeriSS (Automated Verification of Software Systems), ANR "Sécurité et Informatique", 2007-2010.
  • DOTS (Distributed Open and Timed Systems), ANR "Sécurité et Informatique" 2007--2010.
  • PRELUDE (Vers une pragmatique théorique basée sur la ludique et les continuations), ANR, "programme blanc", 2007-2010.
  • DocFlow (Analysis, monitoring and optimisation of Web documents and services), ANR "Masse de Données et Connaissances Ambiantes" 2007-2009.
  • GRAAL (Décompositions de Graphes et Algorithmes), ANR "programme blanc", 2006-2009.
  • SPaCIFY (Ingénierie des modèles et méthodes formelles intégrées pour le développement des logiciels de vol spatiaux), ANR "Technologies logicielles", 2007-2009.
  • RIMEL (Raffinement Incrémental de Modèles événementiels), ANR "Sécurité et Informatique", 2007-2009.
  • A3PAT (Assister Automatiquement Les Assistants de Preuve Avec des Traces), ANR, "Sécurité et Informatique" 2006-2009.
  • CRYSCOE (Cryptographie pour la Sécurité des Codes Embarqués), 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-200
  • MOSAIQUE (Modèles syntaxiques de haut niveau), ARC INRIA, 2006-2007.
  • GDR IM Informatique et Mathématiques.
  • GDR GPL Génie de la Programmation et du Logiciel.


Séminaires :



Liste des Membres de l'équipe


Nom-PrénomEmailTéléphoneBureauStatutWebFonction
Alleg Abdelhamidemail+33 (0)5 40 00 35 17 357 Doct
Archipoff Simonemail+33 (0)5 40 00 35 05 267 Doct
Baschenis Felixemail+33 (0)5 40 00 84 19 123 Doct
Bauderon Michelemail+33 (0)5 40 00 24 95 107 Pr
Billaud Michelemail+33 (0)5 40 00 69 21 213 MdC
Carrere Frederiqueemail+33 (0)5 40 00 84 25 309 MdC
Casteran Pierreemail+33 (0)5 40 00 69 31 304 MdC
Chaabouni Nadiaemail+33 (0)5 40 00 35 31 328 Doct
Courcelle Brunoemail+33 (0)5 40 00 60 86 117 Pr
Dando Louis-marieemail+33 (0)5 40 00 35 17 357 Doct
Durand Irèneemail+33 (0)5 40 00 69 14 204 MdC
Felix Patrickemail+33 (0)5 40 00 69 15 262 MdC
Figueira Diegoemail+33 (0)5 40 00 29 28 209 CR
Fleury Emmanuelemail+33 (0)5 40 00 69 34 261 MdC
Fournier Paulinemail+33 (0)5 40 00 35 04 277 PostDoc
Gauwin Olivieremail+33 (0)5 40 00 38 73 311 MdC
Geffroy Thomasemail+33 (0)5 40 00 84 27 325 Doct
Gimbert Hugoemail+33 (0)5 40 00 84 28 275 CR
Griffault Alainemail+33 (0)5 40 00 69 15 262 MdC
Herbreteau Fredericemail+33 (0)5 40 00 33 36 263 MdC
Hofer Ludovicemail+33 (0)5 40 00 35 15 258 Doct
Janin Davidemail+33 (0)5 40 00 69 16206 MdC
Kelmendi Edonemail+33 (0)5 40 00 84 19 123 Doct
Kirman Jeromeemail+33 (0)5 40 00 37 96 257ATER
Lapoire Denis email+33 (0)5 40 00 69 16 206 MdC
Leroux Jeromeemail+33 (0)5 40 00 35 09 264 DR
Lhote Nathanemail+33 (0)5 40 00 84 19 123 Doct
Lombardy Sylvainemail+33 (0)5 40 00 69 20 254 Pr
Ly Olivieremail+33 (0)5 40 00 84 28 275 MdC
Moot Richardemail+33 (0)5 40 00 29 28209 CR
Mosbah Mohamedemail+33 (0)5 40 00 69 17 363 Pr Directeur Adjoint Resp. Relations Industrielles
Muscholl Ancaemail+33 (0)5 40 00 35 21 321 Pr
Musumbu Kanindaemail+33 (0)5 40 00 38 76 260 MdC Correspondant formation continue master informatique
Nguyen Steveemail+33 (0)5 40 00 38 72 208 PostDoc
Passault Gregoireemail+33 (0)5 40 00 35 94 219 Doct
Pierron Theoemail+33 (0)5 40 00 84 27 325 Doct
Place Thomasemail+33 (0)5 40 00 37 95 278 MdC
Point Geraldemail+33 (0)5 40 00 38 76 260 IR
Puppis Gabrieleemail+33 (0)5 40 00 37 95 278 CR
Renard Matthieuemail+33 (0)5 40 00 35 00 356 Doct
Renault Davidemail+33 (0)5 40 00 35 39122 MdC
Rollet Antoineemail+33 (0)5 40 00 69 08 115 MdC
Rouxel Quentinemail+33 (0)5 40 00 35 94 219 Doct
Sénizergues Géraudemail+33 (0)5 40 00 35 26 312 Pr
Simon Laurentemail+33 (0)5 40 00 37 98 302 Pr
Sutre Gregoireemail+33 (0)5 40 00 33 36263 CR
Tran Thanh-tungemail+33 (0)5 40 00 84 27 325 Doct
Walukiewicz Igoremail+33 (0)5 40 00 69 03 320 DR
Weil Pascalemail+33 (0)5 40 00 84 23 362 DR
Zeitoun Marcemail+33 (0)5 40 00 60 94 202 Pr Directeur adjoint. Responsable de la Licence Informatique.

Page mise à jour le 23/02/2016 à 09:44