Français Anglais
Accueil Annuaire Plan du site
Accueil > Equipes > Activités de recherche > Démonstration automatique, smt et applications
Equipes
Démonstration automatique, smt et applications


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

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


Activités de recherche
° 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
° Calcul à haute performance
° 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
° 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
° Interaction Homme-Machine
° Langages et systèmes centrés données
° Méthodes de conception générative
° Modélisation et systèmes à grande échelle
° Optimisation combinatoire et stochastique