PROTHEO : Contraintes, déduction automatique et preuves de propriétés de logiciels (équipe-projet)

En savoir plus sur l’équipe-projet : Site de l’équipe-projet Rapport d'activité La médiathèque Rapports de recherche Thèses Thème : Sym Systèmes symboliques Centre de recherche Nancy - Grand Est

PROTHEO a été arrêté le 31/12/2007

Présentation de l’équipe-projet

Equipe-projet du LORIA commune avec le CNRS, les universités Henri Poincaré, Nancy 2 et INPL.

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 internationales et industrielles

• 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.

Responsable scientifique

Claude KIRCHNER
+33 3 54 95 84 05
Claude.Kirchner@inria.fr
Secrétariat : +33 3 54 95 84 02