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.
|