Description du groupe LTP

Titre du groupe

Langages, Types et Preuves (LTP)

Responsable(s)

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

• Sylvain Conchon, laboratoire LRI, Université Paris-Saclay, sylvain.conchon@lri.fr   
• Alain Giorgetti, laboratoire FEMTO-ST, Université de Franche-Comté, alain.giorgetti@univ-fcomte.fr

(Anciens responsables : Sandrine Blazy, laboratoire IRISA, Université de Rennes 1, Pierre Castéran, LABRI, Bordeaux, Catherine Dubois ENSIIE, Evry, Marc Pouzet ENS, Paris)

Thématique scientifique

Présentation succincte de la thématique scientifique du groupe.   
   
Les activités de ce groupe répondent aux thèmes suivants du GDR :

• la conception de langages plus sûrs et plus expressifs
• le développement des techniques de vérification et de validation à partir de spécifications ou de code : preuve de correction, analyse statique, génération de tests et raffinements prouvés
• la vérification des outils de développement (interpréteurs, compilateurs, analyseurs statiques, générateurs de code, etc.)
• la vérification d'algorithmes.

En effet, on peut acquérir un grand niveau de confiance sur une application, par exemple :

• en utilisant des langages de programmation de confiance, à la sémantique parfaitement définie, présentant un typage puissant et sûr, réalisant des analyses statiques et des optimisations elles aussi sûres,
• en utilisant des techniques et des outils permettant des raffinements prouvés, sur tout ou une partie du code,
• en prouvant que le code satisfait les propriétés énoncées dans la spécification et en vérifiant ces preuves de manière à fournir des certificats concernant le code,
• en utilisant des langages de haut niveau permettant la modélisation, la validation et la simulation des systèmes,
• en assurant automatiquement la cohérence entre la documentation et le système développé,
• en s'assurant de la correction des outils utilisés dans le cadre du développement.

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 l'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 fondamental (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 volet preuve du groupe concerne non seulement le développement de techniques et outils pour la preuve mais aussi l’utilisation de ces outils dans le cadre du développement de logiciels sûrs. Un des outils utilisés par de nombreux participants du groupe est l’assistant à la preuve Coq mais d’autres outils comme Isabelle, Focal, Dedukti, Cime, des prouveurs automatiques, Why3 (liste non exhaustive) sont développés et/ou utilisés par les membres du groupe.

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

Liste de diffusion

Les messages du groupe LTP sont diffusés sur la liste ltp@groupes.renater.fr. L'abonnement à cette liste s'effectue depuis la page https://groupes.renater.fr/sympa/info/ltp.

Relations avec le GDR IM (Informatique Mathématique)

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 dans le groupe de travail «Logique, Algèbre et Calcul» du GDR IM. 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.  

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.

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

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

• CEA-LIST (Laboratoire de la Sureté du Logiciel, Benjamin Monate)
• Axalto (Équipe Méthodes Formelles et Sécurité, Boutheina Chetali, 3 permanents, 1 doctorant)
• France Telecom R&D (Équipe MAPS/AMS/VVT, Pierre Crégut, 3 permanents et 1 doctorant)
• Trusted Labs (Eduardo Giménez, 3 permanents)
• Dassault Aviation (équipe DGT/DPR/ESA, Dillon Pariente, 1 permanent)

Mode de fonctionnement - Organisation des activités du groupe

Un bureau composé de personnes représentatives des différentes activités décide de l'intégration de nouvelles équipes, de la répartition des crédits.   
   
Le groupe communique à l'aide d'une liste de diffusion et d'une page Web d'information. Il organise 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 peut également proposer des journées de formation aux méthodes et outils développés, en particulier dans le cadre de l'école des jeunes chercheurs.

Le bureau se charge de collecter les informations concernant les thèses en cours dans le groupe ou soutenues récemment de manière à avoir une vue (plus ou moins à jour) des jeunes chercheurs du groupe. Cette information peut aider lors des recrutements de chercheurs, enseignants-chercheurs et post-doctorants.

Conférences ou ateliers associés au groupe

   
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.  

Page Web Page du groupe de travail