Changes for page GT Langages et vérification de programmes (LVP)

Summary

• Page properties (1 modified, 0 added, 0 removed)

Details

Page properties

Content

...	...	@@ -1,79 +1,34 @@
1		-= Description =
	1	+= Objectifs =
2	2
3		-De nombreux formalismes, méthodes et outils existent pour accroître la confiance
4		-dans le logiciel. Toutefois, leurs limites sont bien connues et il reste encore
5		-beaucoup à faire pour relever le défi de la programmation sans bugs. L'objectif
6		-principal de ce groupe de travail est de faire progresser la recherche sur ces
7		-méthodes formelles, le développement de ces outils, et leur diffusion dans
8		-l'industrie, l'enseignement et la recherche.
9		-
10		-Pour parvenir à des programmes exempts de bugs, un axe consiste à proposer des
11		-langages de programmation plus sûrs et mieux sécurisés, interdisant notamment
12		-l'écriture de certaines classes de programmes incorrects. Il est également
13		-possible d'étendre les langages de programmation avec des langages de
14		-spécification permettant d'exprimer formellement tout ou partie des différents
15		-comportements attendus des programmes afin de vérifier la correction de ces
16		-derniers vis-à-vis de leurs spécifications ainsi exprimées. En outre, il est
17		-aussi possible de développer des programmes corrects par construction.
18		-
19		-Par ailleurs, le GT est tout particulièrement concerné par l'application et
20		-l'adaptation des techniques et outils existants à divers domaines de la
21		-recherche actuelle, dont l'informatique théorique et les mathématiques discrètes
22		-
23		-Enfin, pour faciliter l'adaption des méthodes et des outils formels, en
24		-particulier dans l'industrie, il convient notamment de les diffuser auprès des
25		-étudiants des universités et des écoles d'ingénieurs, qui seront les ingénieurs
26		-de demain. Il convient ainsi de réfléchir aux meilleures façons de les enseigner
27		-afin de faciliter leur adoption.
28		-
29	29	Les thèmes du groupe de travail sont :
30	30
31		-* La conception de langages de spécification formelle
32		-* La conception de langages de programmation plus sûrs et mieux sécurisés : systèmes de types, mécanismes de programmation défensive, etc;
33		-* Le développement de techniques de vérification et de validation à partir de
34		- spécifications ou de code : raffinement, preuve de correction, analyses statiques, vérification à
35		- l'exécution, génération automatique de tests, etc;
36		-* La vérification formelle de conjectures, d'algorithmes et de programmes;
37		-* 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;
38		-* Les combinaisons de techniques d'analyse statique et dynamique;
39		-* La diffusion des méthodes formelles dans l'enseignement supérieur et dans l'industrie;
	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.
40	40
41	41	= Porteurs du GT =
42	42
43	43	* Alain Giorgetti, institut FEMTO-ST (UMR CNRS 6174), université de Franche-Comté
44		-* Julien Signoles, CEA LIST
	13	+* Julien Signoles, CEA List
45	45
46	46	= Animations =
47	47
48		-Les actions d'animation envisagées sont :
	17	+Les actions d'animations envisagées
49	49
50		-* Animation du groupe à l'aide d'une liste de diffusion
51		-* Journées scientifiques annuelles de présentation de travaux récents. En fonction du contexte, elles auront lieu en présentiel ou en visioconférence
52		-* Animation d'une session lors des journées du GdR
53		-* Organisation de journées thématiques spécifiques, éventuellement en visioconférence. Un exemple est une journée sur la combinatoire certifiée (développement, formalisation et certification des concepts, des algorithmes et des programmes combinatoires).
54		-* Stimulation de discussions et d'échanges d'informations entre doctorants et chercheurs permanents
55		-
56	56	= Equipes =
57	57
58		- Les équipes impliquées sont :
	21	+ Les équipes impliquées, dont :
59	59
60		-* CEA LIST, Laboratoire de Sûreté et de Sécurité des Logiciels, Saclay
61		-** (//à venir//) permanents impliqués dans le GT
62		-** Représentant : Julien Signoles
	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
63	63
64		-* Equipe VESONTIO, FEMTO-ST/DISC, Besançon
65		-** (//à venir//) permanents impliqués dans le GT
66		-** Représentant : Alain Giorgetti
	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)
67	67
68		-* (//liste en cours d'extension//)
69		-
70		-(//à 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//)
71		-
72	72	= Interactions =
73	73
74		-(//TODO : interactions avec d'autres GTs, GDR, d'autres GTs en cours de construction ou reconstruction//)
75		-
76		-== Autres GDRs
77		-
78		-* GDR IM
79		-* GDR Sécurité. Ce GDR contient notamment un GT "Méthodes formelles pour la sécurité" (https://gtmfsec.irisa.fr/)
	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.