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
  Iris

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
  JOURDAN Jacques-Henri

Thèses et habilitations
  FILLIATRE.02-12-2011
  Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels
  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
° 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
° 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