Proposition de Groupe de Travail pour le GDR GPL

1  Titre du groupe

Langages, Types et Preuves (LTP)

2  Responsable(s)

Nom, affiliation et adresse email des responsables du groupe (pas plus de trois responsables)

Catherine Dubois,
Laboratoire CEDRIC, Institut d'Informatique d'Entreprise, 18 allée Jean Rostand, 91025 Evry,
email : dubois@iie.cnam.fr
Pierre Castéran,
Laboratoire Labri, Université Bordeaux I, 351, cours de la Libération, 33405 Talence,
email : Pierre.Casteran@labri.fr

3  Thématique scientifique

Présentation succincte de la thématique scientifique du groupe.

Les activités de ce groupe répondent aux deux thèmes suivants du GDR En effet, on peut acquérir un grand niveau de confiance sur une application, par exemple : Le groupe étudie des systèmes de types et de preuves et leur application à une programmation sûre. L'enjeu est ici en général la vérification ou inférence des types de manière statique, mais cette vérification statique peut se révéler incomplète, auquel cas on peut alors générer des obligations de preuve ou insérer des tests à l'exécution. Le groupe s'intéressera à différents aspects, aussi bien sur le plan fondement (par exemple spécification d'analyses et propriétés sémantiques) que sur le plan applicatif (détection d'erreurs dans les programmes).

Le groupe comporte un volet autour du développement de l'assistant de preuves Coq, un environnement répondant à la fois aux besoins de mécanisation des preuves mathématiques et à la certification de programmes.

Une autre activité essentielle concerne les outils de preuves automatiques pour la certification de programmes, qui couvrent des problèmes de satisfiabilité modulo des théories (listes, tableaux arithmétiques) pour lesquelles il existe des procédures de décision (cf page SMT-LIB).

Nous voulons avec ce groupe de travail LTP aborder la production de logiciels sûrs sous un angle pratique et sous l'angle langage. Ce groupe est donc complémentaire d'autres groupes de travail comme les groupes AFADL et B par exemple.

Relations avec le GDR Math-info
Les aspects les plus fondamentaux des activités de ce groupe concernant l'étude des systèmes de type, de la logique et des calculs s'intègrent le groupe de travail «Logique, Algèbre et Calcul» du GDR Math-info. L'objectif du groupe de travail LTP est de s'intéresser à la mise en oeuvre des résultats au sein des outils et au développement d'applications.

4  Equipes participantes

Informations sur les équipes françaises participant au groupe de travail:
* Nom de l'équipe
* Laboratoire (éventuellement numéro d'UMR)
* Tutelles du laboratoire
* nombre de permanents, nombre de doctorants et post-doctorants
Nous indiquons pour chaque équipe dans le tableau le nombre de participants à ce groupe de travail, ainsi que le responsable pour cette action.
Équipe Laboratoire Tutelles Responsable Permanents Doctorants Post-docs
ACADIE IRIT, UMR 5505 CNRS, INPT, UPS, UT1 M. Filali 4 2  
ALI UMA ENSTA M. Mauny 1    
Cassis LIFC, FRE 2661, LORIA, UMR 7503 Univ. de Franche-Comté,INRIA Lorraine, CNRS, INPL, Univ. Nancy 1&2 A. Giorgetti, S. Ranise 4 3 1
CPR Cedric, EA 1395 CNAM C. Dubois 8 2  
Démons LRI, UMR 8623 Univ. Paris Sud, CNRS C. Paulin 8 6  
Everest INRIA Sophia-Antipolis INRIA B. Grégoire 3 3 1
Gallium INRIA-Rocquencourt INRIA X. Leroy 3 4  
Lande IRISA, UMR 6074 Univ. Rennes 1, CNRS, INRIA, INSA Rennes Th. Jensen 8 10 1
LCR LIPN, UMR 7030 Université Paris 13, CNRS M. Mayero 8    
LogiCal INRIA Futurs & LIX, UMR 7161 INRIA, École Polytechnique, CNRS B. Werner 6 8 1
Marelle INRIA Sophia-Antipolis INRIA Y. Bertot 5 1  
Méthodes Formelles, CombAlgo LABRI, UMR 5800 Univ. Bordeaux 1 & 2, ENSEIRB, CNRS P. Castéran 4 1  
LIS IBISC, FRE 2873 CNRS, Univ. d'Evry Val d'Essonne, Genopole J-L. Giavitto 2 1  
Move LIF, UMR 6166 CNRS, Univ. Aix-Marseille I et II S. Coupet 1 1  
Plume LIP Ministère, CNRS, ENS Lyon P. Lescanne      
PPS PPS, UMR 7126 CNRS, Univ Paris 7 P. Letouzey 5    
Protheo LORIA INRIA Lorraine, CNRS, INPL, Univ. Nancy 1&2 C. Kirchner 5 10 2
SPI LIP6, UMR 7606 Univ. Paris 6, CNRS Th. Hardin 3 5  

Un point fort commun à la plupart des équipes participantes est leur implication dans des projets de l'ACI Sécurité et Informatique.

5  Equipes étrangères ou industrielles associées au groupe de travail

Mentionner les équipes industrielles ou étrangères qui participeront aux travaux du groupe.

6  Objectifs du groupe de travail - Projets d'actions

Donner ici ce qui constitue la valeur ajoutée par la constitution de ce groupe de travail vis-à-vis de la situation actuelle.

6.1  Langages applicatifs

L'objectif du groupe de travail est de rassembler des équipes travaillant dans le domaine des langages applicatifs c'est-à-dire, de façon large et dans le désordre, les langages ensemblistes, fonctionnels, parenthétiques, à objets ou acteurs, à la fois sur le plan théorique (nouveaux langages ou dialectes, sémantique de nouveaux traits, compilation, interprétation etc.) et pratique (utilisation de ces langages, implantation, gestion de mémoire, algorithmes distribués ou parallèles, mesure de performances, etc.). Un souci croissant dans cette communauté concerne la formalisation et la vérification des propriétés sémantiques attachées aux nouveaux traits de programmation.

Cette activité s'articule autour de l'organisation des « Journées Francophones des Langages Applicatifs ».

6.2  Assistant de preuve Coq

L'assistant de preuve Coq, développé depuis maintenant 20 ans, connait un succès grandissant comme en témoigne la parution récente d'un ouvrage de référence [1] et le nombre grandissant de contributions. L'objectif du groupe de travail dans ce domaine est de permettre les échanges sur le plan national : formations, valorisation des contributions, interactions entre dévelopeurs et utilisateurs...

6.3  Démonstration automatique

La preuve automatique de programmes inclut la vérification statique de types et le déchargement d'obligations de preuve dans des outils de démonstration automatique. L'ambition de cette activité est de relier des langages de spécification et de programmation avec des procédures de décision capables de décharger leurs conditions de correction.

Le groupe de travail rassemble plusieurs équipes qui travaillent déjà sur l'utilisation de méthodes de preuve automatique pour l'ingénierie logicielle. Un objectif est de favoriser les collaborations entre équipes impliquées, en travaillant notamment à la combinaison d'outils de satisfiabilité modulo une théorie (SMT) produisant automatiquement des preuves et d'assistant de preuve interactifs dans le contexte de la vérification de programmes.

Bibliothèques pour des preuves automatiques et des analyses de programme certifiées
Un souci croissant des communautés de démonstration automatique ou d'analyse statique de programmes est la possibilité de garantir la fiabilité des outils développés. C'est un enjeu important dans la mesure où les algorithmes sont généralement complexes à justifier mathématiquement, que leur mise en oeuvre efficace entraine des choix d'implantation sophistiqués et qu'ils sont de plus en plus utilisés pour garantir la correction de programmes critiques. Améliorer la confiance que l'on peut avoir dans ces outils peut se faire en prouvant la correction des programmes eux-mêmes, ou de manière moins ambitieuse en produisant pour chaque problème une justification de sa correction sous forme d'une trace permettant de vérifier a posteriori le résultat obtenu. Il s'agit d'un travail de longue haleine, nous souhaitons au sein de ce groupe de travail favoriser cette approche de la démonstration automatique ou d'analyse statique certifiée en favorisant le développement cohérent et le partage de bibliothèques et d'outils.

Coopération d'outils de preuve
Un enjeu important est de combler progressivement le fossé entre les outils interactifs (Coq par exemple) et des procédures de décision automatiques peu expressives. C'est l'objectif d'un prouveur tel que HaRVey. Le groupe LTP réunissant des chercheurs utilisant et/ou développant des outils de preuve différents (par exemple Coq, Zenon, Harvey), un des thèmes développés concerne l'approche multi-prouveurs.

Il s'agit là de construire de nouveaux prouveurs en combinant judicieusement différentes techniques de démonstration ou encore de faire coopérer des prouveurs en déléguant un sous-problème à un outil mieux adapté pour le résoudre.

Concevoir de nouveaux schémas d'intégration d'outils interactifs et automatiques devrait donner naissance à une nouvelle génération d'outils de raisonnement offrant, entre expressivité et automatisation, un compromis acceptable pour l'application de techniques de vérification déclaratives dans l'industrie.

7  Mode de fonctionnement - Organisation des activités du groupe

Décrire ici comment vous envisagez le fonctionnement du groupe.

Un bureau composé de personnes représentatives des différentes activités se mettra en place. Il décidera de l'intégration de nouvelles équipes, de la répartition des crédits.

Le groupe mettra en place une liste de diffusion et une page WEB d'information. Il se propose d'organiser des journées de travail afin d'améliorer les échanges entre les partenaires et favoriser les réponses à différents programmes nationaux et internationaux. Il proposera également des journées de formation aux méthodes et outils développés en particulier dans le cadre de l'école des jeunes chercheurs.

Journées du groupe LTP
Une journée annuelle réunira l'ensemble des chercheurs du groupe. Une grande place y sera réservée aux doctorants.

Journée Coq
Outre des rencontres de tout le groupe LTP, nous prévoyons dans le cadre de ce groupe de travail d'organiser une journée Coq annuelle, permettant la rencontre des développeurs et des utilisateurs du système Coq et la présentation de contributions (tactiques, bibliothèques, applications) au système.

Contributions Coq
Les développeurs de Coq maintiennent depuis longtemps un dépôt de contributions des utilisateurs, qui fait déjà office de bibliothèque de résultats mathématiques qui peuvent être réutilisés d'une expérience à l'autre. Le groupe de travail établira un protocole de valorisation de cette bibliothèque afin d'en assurer une meilleure reconnaissance. Il s'agira par exemple de mettre en place un mécanisme d'évaluation et de publication électronique et de fournir des guides pour l'intégration des contributions individuelles dans un corpus organisé et cohérent.

8  Conférences ou ateliers associés au groupe

Si le groupe est fortement impliqué dans l'organisation d'une conférence ou d'un atelier, les mentionner dans cette rubrique, ainsi que leur site web.

Le groupe est fortement impliqué dans l'organisation de la conférence nationale JFLA dont les thèmes principaux sont traditionnellement la théorie et les applications pratiques des langages applicatifs, les techniques de développement formel et de certification des algorithmes.

9  Page Web

Si elle existe, donnez l'URL de la page web du groupe de travail.

Page préliminaire

References

[1]
Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Springer-Verlag, 2004.

This document was translated from LATEX by HEVEA.