Equipe de recherche PROTHEO

Contraintes, déduction automatique et preuves de propriétés de logiciels

  • Responsable : Claude Kirchner
  • Centre(s) de recherche : Nancy - Grand Est
  • Domaine : Systèmes symboliques
  • Thème : Sécurité et fiabilité du logiciel

Présentation de l'équipe

L'objectif de l'équipe-projet PROTHEO est la conception et la réalisation d'outils pour la spécification et la vérification de logiciels.

Nous travaillons à un environnement permettant de prototyper de tels outils, à des démonstrateurs spécialisés sur les preuves par récurrence ou dans certaines théories équationnelles, et à des techniques de preuve spécifiques privilégiant l'utilisation des contraintes et des règles de réécriture. L'équipe-projet a trois thèmes de recherche complémentaires : résolution de contraintes, mécanisation de la déduction et démonstration automatique de théorèmes.

Axes de recherche

  • Résolution de contraintes.
    • Contraintes symboliques et numériques.
    • Collaboration de solveurs.
    • Techniques de propagation, consistance et énumération.
  • Mécanisation de la déduction par règles et stratégies.
    • Langage de stratégies pour résolveurs et démonstrateurs.
    • Calculs non déterministes.
    • Compilation de la réécriture et des stratégies.
    • Propriétés de confluence, terminaison, modularité.
  • Démonstration automatique de théorèmes.
    • Déduction automatique avec contraintes.
    • Preuves par récurrence.
    • Preuves de propriétés observables.
    • Preuves de propriétés de programmes.
L'équipe développe plusieurs logiciels, en particulier Spike (un logiciel d'étude du raisonnement par récurrence et de preuves en logique du premier ordre), Elan (un cadre logique pour prototyper résolveurs de contraintes et processus de déduction) et daTac (un logiciel de preuve dans les théories associatives commutatives).

Relations industrielles et internationales

  • Participation aux projets Esprit Basic Research CCL et Working Group CoFI, au réseau d'excellence Compulog, et à des groupes de travail ERCIM
  • Coopération via NSF avec l'université d'Illinois à Urbana-Champaign (Etats-Unis).
  • échanges avec des centres de recherche : Max Planck Institut fur Informatik (MPI), DFKI, CWI, SRI International et avec des universités : Aarhus, Amsterdam, Kaiserslautern, Porto, Saarbrucken, Taiwan.
  • Contrats avec le Cnet et le GIHP Champagne.

Mots-clés : Spécification formelle Vérification du logiciel Démonstration automatique Mécanisation de la déduction Résolution de contraintes Réécriture

Siège et centres de recherche Inria

Accès direct

Social