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 :