Formal Methods
Head : J. LerouxMembres Publications




Research themes :

The Formal Methods team is active in many areas of theoretical computer science and its applications. Its work is grouped in two themes:

  • Logiques, graphes et langages (LGL)
    • Head: S. Lombardy.
    • Keywords: Graph decompositions, recognizability, monadic second order logic, mu calculus, lambda calculus, games, proof assistants, finite descriptions of countable objects.
  • Modélisation et vérification (MV)
    • Head: L. Simon.
    • Keywords: Verification, synthesis, infinite state systems, concurrent systems, real-time, data formalisms, symbolic representations, analysis of binary code.



Research report 2009-2014 (PDF)



----

Events:

  • JFPC'15 (Journées Francophones de Programmation par Contraintes), June 22-24, 2015.
  • ALFA'15 (Automata, logic, formal languages and algebra), June 15-17, 2015.
  • RP'12, 6th International workshop on Reachability Problems, September 17-19, 2012.
  • Workshop Bruno Courcelle, June 18-20, 2012.
  • EPIT'11, GAMES-Spring school. Carcans-Maubuisson, May 23-27, 2011.
  • LCS'10, workshop "Logic, categories, semantics", November 2010.
  • STACS'08, Symposium on Theoretical Aspects of Computer Science, February 2008.
  • AltaRICA'07, workshop of AltaRICA users and developers, November 2007.
  • MOVEP'06, MOdelling and VErifying parallel Processes, June 2006.


Software:

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


Projects:

  • 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 (Parsing and synthesis with abstract categorial grammars: from lexicon to discourse), ANR CONTINT, 2012-2015.
  • LOCI (Locativity and interactivity in logic, linguistics and theoretical computer science), ANR BLANC, 2010-2014.
  • SAFE (Safe Automotive soFtware architEcture), UE project, 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, FUI project (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 GDR Informatics and Mathematics.
  • GDR GPL GDR Software and Program Engineering.


Seminar: