Formal Methods
Head : A. MuschollMembres Publications




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:

  • Logique, linguistique et informatique (LLI) (closed in June 2014)
    • 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: I. Walukiewicz.
    • 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: M. Zeitoun.
    • Keywords: Verification, synthesis, infinite state systems, concurrent systems, real-time, data formalisms, symbolic representations, analysis of binary code.



Rapport d'activité 2008 (in French) (PDF)



----

Events:

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

  • 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.
  • XFLG: Implantation d’un analyseur pour grammaire LFG.


Projects:

  • ANR Stoch-MC, Modèles stochastiques: passage à l’échelle pour le Model Checking, ANR Blanc, 2014-2018.
  • ANR ExStream, Extensions of streaming processing, 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
  • 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.


Seminars:



Liste des Membres de l'équipe


Nom-PrénomEmailTéléphoneBureauStatutWebFonction
Baschenis Felixemail+33 (0)5 40 00 84 19 123 Doct
Bauderon Michelemail+33 (0)5 40 00 24 95 107 Pr
Ben-jaballah Wafaemail+33 (0)5 40 00 35 54 125 IR
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 Responsable Emplois du Temps Licence Informatique
Courcelle Brunoemail+33 (0)5 40 00 60 86 117 Pr
Cudeville Brigitteemail+33 (0)5 40 00 60 90 176Adjoint Technique
Dicky Anneemail+33 (0)5 40 00 69 16 206 MdC
Dubourg Etienneemail+33 (0)5 40 00 84 15 274 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
Fontaine Allyxemail+33 (0)5 40 00 69 37 327 Doct
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 257 Doct
Lapoire Denis email+33 (0)5 40 00 69 29 207 MdC
Leroux Jeromeemail+33 (0)5 40 00 35 09 264 CR
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
Passault Gregoireemail+33 (0)5 40 00 35 94 219 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 20 356 Doct
Renault Davidemail+33 (0)5 40 00 35 39122 MdC
Retore Christianemail+33 (0)5 40 00 38 72 208 Pr
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
Salvati Sylvainemail+33 (0)5 40 00 35 23 210 CR
Sandillon-rezer Noemie-fleuremail+33 (0)5 40 00 37 96 257ATER
Simon Laurentemail+33 (0)5 40 00 37 98 302 Pr
Sutre Gregoireemail+33 (0)5 40 00 33 36263 CR
Sylvestre Marcemail+33 (0)5 40 00 35 54 125ATER
Totzke Patrickemail+33 (0)5 40 00 35 05 267 PostDoc
Tran Thanh-tungemail+33 (0)5 40 00 84 27 325 Doct
Van Rooijen Lorijnemail+33 (0)5 40 00 35 31 328 Doct
Vincent Aymericemail+33 (0)5 40 00 35 09264 MdC
Walukiewicz Igoremail+33 (0)5 40 00 69 03 320 DR
Weil Pascalemail+33 (0)5 40 00 69 10 174 DR Directeur
Zeitoun Marcemail+33 (0)5 40 00 60 94 202 Pr

Page mise à jour le 14/10/2014 à 12:08