Français Anglais
Accueil Annuaire Plan du site
Accueil > Equipes > Activités de recherche > Vérification déductive de programmes
Equipes
Vérification déductive de programmes



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

Equipes-projets Inria communes
  Toccata

Resultats majeurs
  Formal firewall conformance testing: an application of test and proof techniques

Contrats
  HISSEO
  U3CAT
  Bware
  VERASCO
  HI-LITE
  CIFRE ADACORE

Logiciels et brevets
  Alt-Ergo
  Frama-C
  CFML

Collaborations
  CEA-LIST
  AdaCore SAS

Membres
  FILLIÂTRE Jean-Christophe
  MARCHÉ Claude
  PAULIN-MOHRING Christine
  BOLDO Sylvie
  PASKEVYCH Andriy
  MELQUIOND Guillaume
  TAFAT BOUZID Asma
  CHARGUERAUD Arthur
  CLOCHARD Martin
  GONDELMANS Levs
  BALABONSKI Thibaut
  MBIADA NDJANDA Jacques Charles

Thèses et habilitations
  FILLIATRE.02-12-2011
  Un langage unique pour à la fois développer des programmes et les prouver
  Preuves par raffinement de programmes avec pointeurs
  Un système de types pragmatique pour la vérification déductive des programmes


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
° Démonstration automatique, SMT et applications
° 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