Mots-clés:
  - Diagnostic
  - Preuve de programme
  - Test de logiciels
  - Model-checking
  - Arithmétique flottante

Equipes
  Algorithmique et Complexité
  Toccata
  Test Formel et Exploration de Systèmes

Equipes-projets Inria communes


Resultats majeurs
  Exploration Uniforme de très grands modèles
  HOL-Boogie - An Interactive Prover-Backend for the Verified C Compiler
  One step forward: Linking wireless self-organizing network validation techniques with formal testing approaches
  On Theorem Prover-based Testing

Contrats
  CAT
  CIFRE DASSAULT
  Usine Logicielle
  VERAP
  GECCOO
  HOL-TestGen XT

Logiciels et brevets
  sALLUSTe
  RUKIA
  CFML

Collaborations


Membres
  MAGNIEZ Frédéric
  VIEILLERIBIERE Adrien
  GOURAUD Sandrine
  MESSIKA Stéphane
  FAYOLLE Julien
  STOULS Nicolas
  TRACOL Mathieu
  PEYRONNET Sylvain
  OUDINET Johan
  BARDOU Romain
  LESCUYER Stéphane
  BENTAKOUK Lina
  URRIBARRI Wendi
  LASSAIGNE Richard
  LALLALI Mounir

Thèses et habilitations
  Preuves mécanisées de propriétés de programmes
  Utilisation des Structures Combinatoires pour le Test Statistique
  Vérification approchée - Calcul quantique
  Observer la stabilisation
  Auto-test pour les calculs approché et quantique
  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