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

Equipes-projets Inria communes
  Toccata

Resultats majeurs
  ESOP 2014 : A Coq Formalization of the Relational Data Model
  Formal firewall conformance testing: an application of test and proof techniques

Contrats
  HISSEO
  Typex
  Paral-ITP
  EURO-MILS
  VERASCO
  DIM COQUELICOT
  HI-LITE

Logiciels et brevets
  HOL-TestGen
  HOL-OCL
  Le Système HOL-Z
  ALEA
  Isabelle/HOL
  The Coquelicot library
  CFML
  OntoEvent-B
  Pactole

Collaborations
  MBTSEC
  System X FSF

Membres
  BENZAKEN Véronique
  CONTEJEAN Evelyne
  MARCHÉ Claude
  PAULIN-MOHRING Christine
  BOLDO Sylvie
  MANDEL Louis
  URBAIN Xavier
  WOLFF Burkhart
  LONGUET Delphine
  LELAY Catherine
  CHARGUERAUD Arthur
  DUMBRAVA Stéfania Gabriela
  NEMOUCHI Yakoub
  TUONG Frédéric
  BALABONSKI Thibaut
  NGUYEN VAN Hai
  AIT-SADOUNE Idir
  VALIRON Benoît
  JOURDAN Jacques-Henri

Thèses et habilitations
  Formalisation en Coq de Bases de Données Relationnelles et Déductives - et Mécanisation de Datalog
  Model-Based Testing of Operating System-level Security Mechanisms
  Constructing Semantically Sound Object-Logics for UML/OCL Based Domain-Specific Languages
  De nouveaux réels pour Coq

° 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
° Démonstration automatique, SMT et applications
° Distributed Design
° Fab lab
° Fabrication Numérique
° 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