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)

Sandrine Blazy,
Laboratoire IRISA, Université de Rennes 1, Campus de Beaulieu, 35042 Rennes cedex,
email : sandrine.blazy@irisa.fr
Marc Pouzet,
Laboratoire LIENS, ENS? 45 rue d'Ulm, 75005 Paris,
email : Marc.Pouzet@ens.fr

(Anciens responsables : Catherine Dubois ENSIIE Evry, Pierre Castéran Labri, Bordeaux)

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

  • 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 staitiques, 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 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 volet preuve du groupe concerne non seulement de 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, Why (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 MTVV 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.
 

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.

ÉquipeLaboratoireTutellesResponsablePermanentsDoctorantsPost-docs
ACADIEIRIT, UMR 5505CNRS, INPT, UPS, UT1M. Filali42 
ALIUMAENSTAM. Mauny2  
APRLIP6Université Paris 6, CNRSE. Chailloux44 
CassisLIFC, FRE 2661, LORIA, UMR 7503Univ. de Franche-Comté,INRIA Lorraine, CNRS, INPL, Univ. Nancy 1&2A. Giorgetti, S. Ranise431
CeltiqueIRISA, UMR 6074Univ. Rennes 1, CNRS, INRIA, INSA RennesT. Jensen8101
CPRCedric, EA 1395CNAMC. Dubois82 
DeducteamiNRIA RocquencourtINRIAG. Dowek242
DémonsLRI, UMR 8623Univ. Paris Sud, CNRSC. Paulin86 
EverestINRIA Sophia-AntipolisINRIAB. Grégoire331
FormesLIAMAINRIAJ.P. Jouannaud231
FortesseLRI, UMR 2623Université Paris Sud, CNRSB. Wolff641

Gallium

INRIA-RocquencourtINRIAX. Leroy34 
IGGLSIIT, UMR 7005Univ. Louis Pasteur, CNRSN. Magaud3  
LCRLIPN, UMR 7030Université Paris 13, CNRSM. Mayero8  
LogiCalINRIA Futurs & LIX, UMR 7161INRIA, École Polytechnique, CNRSB. Werner681
Logique et ProgrammationLACL, EA 4219Université Paris XIIO. Michel200
LISIBISCUniversité d'EvryS. Cerrito2  
LSLCEA J. Signoles53 
MarelleINRIA Sophia-AntipolisINRIAY. Bertot51 
Méthodes FormellesLABRI, UMR 5800Univ. Bordeaux 1 & 2, ENSEIRB, CNRSP. Castéran41 
ParkasLIENS, INRIAENS, INRIAM. Pouzet32 
PlumeLIPMinistère, CNRS, ENS LyonP. Lescanne   
PiR2PPS, UMR 7126CNRS, Univ Paris 7P. Letouzey5  
ProtheoLORIAINRIA Lorraine, CNRS, INPL, Univ. Nancy 1&2C. Kirchner5102
SPILIP6, UMR 7606Univ. Paris 6, CNRSTh. Hardin20 

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 mettra en place une liste de diffusion et une page WEB d'information. Il se propose de continuer à 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

Le bureau se chargera de collecter les informations concernant les thèses en cours dans le groupe ou soutenues r 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