Sites Inria

English version

Equipe de recherche PROVAL

Preuve de programmes

  • Responsable : Christine Paulin-mohring
  • Centre(s) de recherche : CRI Saclay - Île-de-France
  • Domaine : Algorithmique, programmation, logiciels et architectures
  • Thème : Programmation, vérification et preuves
  • Partenaire(s) : Université Paris-Sud (Paris 11),CNRS
  • Collaborateur(s) : U. PARIS 11 (P.-SUD), CNRS

Présentation de l'équipe

L'objectif de l'équipe-projet de recherche PROVAL est de proposer des méthodes et outils qui s'intègrent dans le cycle de développement de logiciel et qui permettent la production d'un code prouvé correct par rapport à un comportement attendu.

Ce projet, issu de l'équipe-projet LOGICAL, s'appuie sur le formalisme de la théorie des types qui donne un cadre sémantique clair pour représenter en machine les preuves et les calculs.

L'équipe-projet développe un environnement générique de preuve de programmes (Why), qui permet d'engendrer des obligations de preuves qui peuvent être ensuite déléguées à des démonstrateurs automatiques ou interactifs. Sur cet outil, sont construits des environnements dédiés pour prouver des programmes C (Frama-C) et Java (Krakatoa) annotés par des formules décrivant le comportement attendu. L'équipe-projet est également spécialisée dans la preuve de comportement des calculs en nombres flottants.

Axes de recherche

  • Modèles et méthodes de preuve de programmes
    Nous développons des modèles des langages de programmation et des langages de spécification qui répondent aux besoins des applications critiques et se prêtent à la preuve interactive ou automatique. En particulier, nous nous intéressons à la modélisation de constructions abstraites d'ordre supérieur, de manipulation de pointeurs et de l'arithmétique des nombres flottants.
  • Architecture des environnements de preuves de programmes
    La mise en pratique de nos méthodes dans les outils pose des problèmes de passage à l'échelle dans la génération d'obligations de preuve, de méthodologie d'écriture d'annotations, d'expressivité des langages de spécifications et d'assistance au développement de spécification.
  • Démonstration automatique
    La preuve de programmes nécessite d'adapter et de spécialiser des démonstrateurs généraux. L'équipe-projet étudie plus particulièrement les preuves de terminaison ainsi que la combinaison de procédures de décision. Une attention particulière est portée sur la correction de ces techniques.
  • Applications
    Les techniques développées dans l'équipe-projet trouvent leur application dans les domaines qui requièrent le développement de logiciels critiques pour lesquels le besoin de certification est important, en particulier les secteurs bancaires, aéronautique et télécommunications. Nous visons la preuve de code embarqué en C ou en Java ainsi que la certification d'outils de génération de code.

Logiciels

Mots-clés : Preuve de programmes Spécification Démonstration automatique Arithmétique des nombres flottants

Suivez Inria