LTP PDF Imprimer
Statiques
Écrit par Pierre Castéran   

Titre du groupe

Langages, Types et Preuves (LTP)

Responsable(s)

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

Catherine Dubois,
Laboratoire CEDRIC, ENSIIE, 1 square de la résistance, 91025 Evry,
email : Cette adresse email est protégée contre les robots des spammeurs, vous devez activer Javascript pour la voir.
Marc Pouzet,
Laboratoire LIENS, ENS? 45 rue d'Ulm, 75005 Paris,
email : Cette adresse email est protégée contre les robots des spammeurs, vous devez activer Javascript pour la voir.

(Ancien responsable : 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.

É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 2
APR LIP6 Université Paris 6, CNRS E. Chailloux 4 4
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
Celtique IRISA, UMR 6074 Univ. Rennes 1, CNRS, INRIA, INSA Rennes T. Jensen 8 10 1
CPR Cedric, EA 1395 CNAM C. Dubois 8 2
Deducteam iNRIA Rocquencourt INRIA G. Dowek 2 4 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
Formes LIAMA INRIA J.P. Jouannaud
2 3
1
Fortesse LRI, UMR 2623 Université Paris Sud, CNRS B. Wolff 6 4 1

Gallium

INRIA-Rocquencourt INRIA X. Leroy 3 4
IGG LSIIT, UMR 7005
Univ. Louis Pasteur, CNRS
N. Magaud
3
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
Logique et Programmation LACL, EA 4219 Université Paris XII O. Michel 2 0 0
LIS IBISC Université d'Evry S. Cerrito 2
LSL CEA J. Signoles 5 3
Marelle INRIA Sophia-Antipolis INRIA Y. Bertot 5 1
Méthodes Formelles LABRI, UMR 5800 Univ. Bordeaux 1 & 2, ENSEIRB, CNRS P. Castéran 4 1
Parkas LIENS, INRIA ENS, INRIA M. Pouzet 3 2
Plume LIP Ministère, CNRS, ENS Lyon P. Lescanne
PiR2 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 2 0

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

Mise à jour le Mardi, 12 Mars 2013 13:24