Mots-clés:
  - Réécriture

Equipes
  Vérification d'Algorithmes, Langages et Systèmes

Equipes-projets Inria communes
  Toccata

Resultats majeurs
  EATCS Award for Best ETAPS Paper 2011
  Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems

Contrats
  U3CAT
  Bware
  HI-LITE
  CIFRE ADACORE
  GDR7161/G673

Logiciels et brevets
  Alt-Ergo
  Gappa

Collaborations
  CEA-LIST
  AdaCore SAS

Membres
  CONTEJEAN Evelyne
  MARCHÉ Claude
  CONCHON Sylvain
  ZAIDI Fatiha
  URBAIN Xavier
  PASKEVYCH Andriy
  MELQUIOND Guillaume
  IGUERNELALA Mohamed
  MEBSOUT Alain
  DROSS Claire
  MARCOZZI Michaël

Thèses et habilitations
  Renforcement du noyau d'un démonstrateur SMT : conception et implantation de procédures de décision efficaces
  Procédures de Décision Génériques pour des Théories Axiomatiques du Premier Ordre
  Inférence d'invariants pour le model checking de systèmes paramétrés

° Algorithmes pour les grands volumes de données distribuées
° Algorithmique des systèmes en réseau
° Algorithmique distribuée
° Architectures parallèles
° biologie de synthese
° Biologie des systèmes
° Biologie structurale
° biologie synthetique
° Calcul à haute performance
° Calcul quantique
° Calibration d'algorithmes (sélection, ajustement d'hyper-paramètres)
° Codage réseau
° Collaboration médiatisée
° Combinatoire
° Compilation et optimisation des programmes
° Décision optimale en contexte incertain
° Définition de nouveaux critères
° Distributed Design
° Fab lab
° Fabrication Numérique
° Formalisation de langages (de spécification et de programmation) dans les assistants de preuve
° Formalisation et preuves de programmes numériques
° Gestion de données du Web
° Ingénierie des systèmes interactifs
° Intégration de données et de connaissances