Skip to Content
Last modified by Julien Signoles on 2024/02/07 13:55
From version 2.1
edited by Alain Giorgetti
on 2020/06/02 17:50
Change comment: There is no comment for this version
To version 2.4
edited by Alain Giorgetti
on 2020/06/03 19:34
Change comment: There is no comment for this version

Summary

Details

Page properties
Content
... ... @@ -1,11 +1,20 @@
1 -= Objectifs =
1 += Description =
2 2  
3 +De nombreux formalismes, méthodes et outils existent pour accroître la confiance dans le logiciel. Toutefois, leurs limites sont bien connues et il reste encore beaucoup à faire pour relever le défi de la programmation sans bugs. L'objectif principal de ce groupe de travail est de faire progresser la recherche sur ces méthodes formelles, le développement de ces outils, et leur diffusion dans l'industrie, l'enseignement et la recherche.
4 +
5 +Un axe privilégié est l'application et l'adaptation des techniques et outils existants à divers domaines de la recherche actuelle, dont l'informatique théorique et les mathématiques discrètes.
6 +
7 +//(à venir : paragraphe sur l'enseignement des méthodes formelles)//
8 +
3 3  Les thèmes du groupe de travail sont :
4 4  
5 -* La conception de langages plus sûrs et plus expressifs;
6 -* 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;
7 -* La vérification des outils de développement : interpréteurs, compilateurs, analyseurs statiques, générateurs de code, etc;
8 -* La vérification de conjectures, d'algorithmes et de programmes.
11 +* La conception de langages de spécification formelle et de programmation plus sûrs et plus expressifs;
12 +* Le développement de techniques de vérification et de validation à partir de spécifications ou de code : preuve de correction, analyses statiques, raffinement, génération automatique de tests, etc;
13 +* La preuve formelle de conjectures, d'algorithmes et de programmes;
14 +* La vérification des méthodes et outils de développement et de vérification eux-mêmes : interpréteurs, compilateurs, analyseurs statiques, générateurs de code, générateurs de tests, etc;
15 +* Les combinaisons de techniques d'analyse et de vérification statique et dynamique;
16 +* Les applications des méthodes formelles de vérification de conjectures et de programmes;
17 +* La diffusion des méthodes formelles dans l'enseignement supérieur et dans l'industrie;
9 9  
10 10  = Porteurs du GT =
11 11  
... ... @@ -14,21 +14,31 @@
14 14  
15 15  = Animations =
16 16  
17 -Les actions d'animations envisagées
26 +Les actions d'animation envisagées sont :
18 18  
28 +* Animation du groupe à l'aide d'une liste de diffusion
29 +* Journées scientifiques annuelles de présentation de travaux récents, en présence ou en visioconférence
30 +* Animation d'une session lors des journées du GdR
31 +* Stimulation de discussions et d'échanges d'informations entre doctorants et chercheurs permanents
32 +
33 +Sur le plan thématique, le groupe animera une action spécifique de développement de la formalisation et de la certification des concepts, des algorithmes et des programmes de la combinatoire.
34 +
19 19  = Equipes =
20 20  
21 - Les équipes impliquées, dont :
37 + Les équipes impliquées sont :
22 22  
23 -* Equipe AA, Laboratoire, Lieu
24 -** le nombre de permanents impliqués dans le GT et
25 -** le nom d'un représentant dans l’équipe
39 +* CEA LIST, Laboratoire de Sûreté et de Sécurité des Logiciels, Saclay
40 +** (//à venir//) permanents impliqués dans le GT
41 +** Représentant : Julien Signoles
26 26  
27 -(A faire ; sur la page (https:~/~/gdrgpl.myxwiki.org/xwiki/bin/view/Maps/)  : un positionnement de l’équipe sur la carte en
28 -faisant référence à ce  GT dans la description de l’équipe)
43 +* Equipe VESONTIO, FEMTO-ST/DISC, Besançon
44 +** (//à venir//) permanents impliqués dans le GT
45 +** Représentant : Alain Giorgetti
29 29  
47 +* (//liste en cours d'extension//)
48 +
49 +(//à faire sur la page ([[https://gdrgpl.myxwiki.org/xwiki/bin/view/Maps/]]) : positionnement de chaque équipe sur la carte en faisant référence à ce GT dans la description de l'équipe//)
50 +
30 30  = Interactions =
31 31  
32 -Avec d'autres GTs, GDR, ...
33 -Si des GT identifient dès à présent des interactions avec d’autres GTs en cours de construction ou reconstruction ils le
34 -précisent.
53 +(//à venir : interactions avec d'autres GdR et leurs GTs, et avec d'autres GTs en cours de construction ou reconstruction//)