Equipes
  Toccata

Equipes-projets Inria communes


Resultats majeurs
  Formal Verification of Floating-Point Programs

Contrats
  CAT
  CerPAN
  SCALP
  CIFRE DASSAULT
  GECCOO
  FOST
  HISSEO
  DECERT
  CeProMi
  FVOOS

Logiciels et brevets
  Caduceus
  Krakatoa
  Program
  Frama-C
  Gappa
  Coq.FP2
  ALEA
  Flocq Library

Collaborations


Membres
  HUBERT Thierry
  SOZEAU Matthieu
  MOY Yannick
  STOULS Nicolas
  BARDOU Romain
  KANIG Johannes
  LESCUYER Stéphane
  URRIBARRI Wendi

Thèses et habilitations
  Preuves mécanisées de propriétés de programmes
  Preuve automatique et modulaire de la sûreté de fonctionnement des programmes C

° 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 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