Détail d'une fiche   Version PDF

PROTHEO (SR0277VR)

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

PROTHEO →  PAREO (SR0418ER)


Statut: Terminée

Responsable : Claude Kirchner

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : Aucun mot-clé.

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : Aucun mot-clé.

Domaine : Systèmes symboliques
Thème : Sécurité et fiabilité du logiciel

Période : 01/01/1992 -> 31/12/2007
Dates d'évaluation :

Etablissement(s) de rattachement : <sans>
Laboratoire(s) partenaire(s) : <sans UMR>

CRI : Centre Inria de l'Université de Lorraine
Localisation : Centre Inria de l'Université de Lorraine
Code structure Inria :

Numéro RNSR : 199221357D
N° de structure Inria: SR0277VR

Présentation

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.