Equipes (Thèmes de recherche) - Laboratoire de Recherche en Informatique

Equipe Preuve de programmes (Proval)

L'objectif de l'équipe Démons est de proposer des méthodes et des outils pouvant s'intégrer dans le cycle de développement logiciel et permettant de produire du code correct vis-à-vis de comportements attendus.

L'équipe développe une plateforme générique de vérification de programmes (la platforme Why), qui produit des obligations de preuve à partir de programmes annotés de spécifications formelles et les transmet ensuite à des outils de preuve, interactifs ou automatiques. Des instances pour les langages C (Caduceus) et Java (Krakatoa) sont bâties sur cette infrastructure générique.

Site web de l'equipe

Publications de l'equipe

Rapport d'activité 2005-2008

Composition de l'équipe
  Responsable
    PAULIN-MOHRING Christine

  Membres permanents
    BENZAKEN Véronique
    BOLDO Sylvie
    CONCHON Sylvain
    CONTEJEAN Evelyne
    FILLIÂTRE Jean-Christophe
    MANDEL Louis
    MARCHÉ Claude
    MELQUIOND Guillaume
    NGUYEN Kim
    PASKEVYCH Andriy
    PAULIN-MOHRING Christine
    PUEL Laurence

  Membres non-permanents
    BOBOT François
    COUSINEAU Denis
    DOGGUY Mehdi
    DROSS Claire
    HERMS Paolo
    IGUERNELALA Mohamed
    LELAY Catherine
    MEBSOUT Alain
    NGUYEN Thi Minh Tuyen
    ROUX Cody
    TAFAT BOUZID Asma

  Associés
    BRICQUET Régine
    GUESDON Maxence
    URBAIN Xavier

  Stagiaires
    YUAN Shuai

Thèmes de recherche
  Démonstration automatique
  Vérification
  Preuve de programme
  Programmation fonctionnelle
  Logique
  Réécriture
  Théorie des types
  Langages d'ordre supérieur
  Programmation synchrone
  Algorithmique
  Algorithmes probabilistes
  Programmation orientée objet
  Langages centrés données

Projet(s) associé(s)
  ProVal

Contrats en cours
  PARTOUT
  Hi-LITE
  Typex

Logiciels et brevets
  Why : La plateforme Why
  bibtex2html : Traducteur BibTeX vers HTML
  Alt-Ergo : Démonstrateur automatique Alt-Ergo
  ocamlgraph : bibliothèque de graphes pour Ocaml
  Caduceus : Outil Caduceus de vérification de programmes C
  Krakatoa : Outil Krakatoa de vérification de programmes Java
  ReactiveML : le langage ReactiveML
  Lucid Synchrone : Lucid Synchrone
  Program : Program : un langage de programmation avec types dépendants dans Coq
  CiME : CiME, une boîte à outils pour la démonstration automatique.
  CDuce : CDuce an XML centric Functional Programmimg Language
  Mlpost : Mlpost, une interface Objective Caml pour Metapost
  Frama-C : Framework for Modular Analysis of C
  Gappa : Outil Gappa de certification de programmes numériques
  Coq.Interval : Bibliothèque Coq.Interval de preuve automatique de bornes sur des expressions à valeurs réelles
  Coq.FP2 : Coq.FP2
  ALEA : ALEA : A library for reasoning on random algorithms in Coq
  Coccinelle : Coccinelle
  Flocq Library : Flocq Library

Thèses et habilitabions récentes
  Logique de séparation et vérification déductive
  Vérification de programmes avec pointeurs à l'aide de régions et de permissions
  Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq