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, sandrine.blazy@irisa.fr
  • 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 : Marc Pouzet ENS, Paris, 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 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 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, 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.
 

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 
CeltiqueIRISA, UMR 6074Univ. Rennes 1, CNRS, INRIA, INSA RennesT. Jensen8101
CPRCedric, EA 1395CNAMC. Dubois82 
DeducteamiNRIAINRIAG. Dowek242
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  
SPILIP6, UMR 7606Univ. Paris 6, CNRSTh. Hardin20 
VALSLRI, UMR 8623Univ. Paris Sud, CNRSE. Contejean18125
VeriDisLORIA, UMR 7503, INRIA
LORIA,
Univ. de Lorraine, INRIA Nancy, CNRS
S. Merz751

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.

Le bureau se chargera 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