Sites Inria

English version

Equipe de recherche PARSIFAL

Recherche de preuve et raisonnement sur des spécifications logiques

Présentation de l'équipe

L'équipe-projet PARSIFAL a pour but d'élaborer des méthodes et des outils pour la spécification et le raisonnement sur des systèmes calculatoires comme, par exemple, des compilateurs, des protocoles de sécurité et des programmes concurrents. Le défi est ici la preuve de propriétés de programmes qui manipulent d'autres programmes.

Un système calculatoire est aujourd'hui le plus souvent spécifié par une sémantique opérationnelle, elle-même donnée par un ensemble de règles d'inférence définissant des relations. Les sémantiques statiques des langages de programmation (inférence de types, par exemple) sont souvent données de la même manière, par des règles d'inférence).

Le présent projet exploite les développements récents dans les domaines de la théorie des preuves, de la programmation logique et des théories typées dans le but d'exécuter et de raisonner sur des spécifications en sémantique opérationnelle.

Axes de recherche

  • Théorie :nous exploitons la technique de recherche de preuves dans des logiques très expressives pour la spécification de procédés calculatoires. Nous développons également un cadre logique pour spécifier la recherche de preuves. Cette logique est basée sur une logique intuitioniste d'ordre supérieur et inclut des principes d'induction et de co-induction. Nous considérons également sa contre-partie sous la forme d'une théorie typée.
  • Applications: notre travail est dirigé par les applications. Nous nous proposons de développer des composants pour la déduction pouvant être utilisés dans des "model-checkers", des systèmes de bisimulation, des vérificateurs de types ou de preuves, des assistants à la preuve spécialisés, etc. De tels outils de déduction pourront être incorporés dans d'autres systèmes pour permettre de mélanger raisonnement et calcul. Les domaines d'applications typiques sont la sécurité, le "global computing", le "proof-carrying code" et le code mobile.
  • Prototypes: nous nous proposons de développer différents composants utilisés dans l'implémentation de la recherche de preuves (l'unification, la recherche de données, la tabulation, la liaison et la substitution, etc). Ces composants seront utilisés dans l'implémentation de prototypes de recherche avec des applications qui mélangent le calcul et la déduction.

Relations industrielles et internationales

  • Mobius (Mobility, Ubiquity and Security) est un project européen intégré de l'initiative proactive "FET Global Computing".
  • Slimmer (Implémentations Logiques Sophistiquées pour la Modélisation et le Raisonnement Mécanisé) est une "Équipe Associée" de l'INRIA. Gopalan Nadathur, de l'université du Minnesota (États-Unis), dispose d'un budget NSF spécifique pour ce projet.
  • Vallauris est un projet "PAI" (programme d'actions intégrées) du Programme Picasso 2005 de l'Égide. Le titre du projet Vallauris est: intégration de techniques de preuves et d'outils sémantiques dans le "Proof Carrying Code" et validation et analyse de code écrit de manière déclarative.
  • Rossignol est un projet "ACI-Securité" dédié à la vérification de protocoles cryptographiques.
  • GeoCal est une "ACI-Nouvelles interfaces des mathematiques". GeoCal réunit 10 groupes de recherches en logique, en informatique théorique et en topologie algebrique.
  • The Types European project est la continuation d'une série de différents projets Types depuis 1992. Le projet réunit 35 sites autour du développement de la technologie du raisonnement formel et de la programmation basées sur les théories typées.

Suivez Inria tout au long de son 50e anniversaire et au-delà !