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

Summary

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

Details

Page properties

Title

...	...	@@ -1,1 +1,1 @@
1		-GT Langages et vérification de théorèmes et de programmes (LVTP)
	1	+GT Langages et vérification de programmes (LVP)

Content

...	...	@@ -1,34 +1,79 @@
1		-= Objectifs =
	1	+= Description =
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	+
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.
	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;
9	9
10	10	= Porteurs du GT =
11	11
12	12	* Alain Giorgetti, institut FEMTO-ST (UMR CNRS 6174), université de Franche-Comté
13		-* Julien Signoles, CEA List
	44	+* Julien Signoles, CEA LIST
14	14
15	15	= Animations =
16	16
17		-Les actions d'animations envisagées
	48	+Les actions d'animation envisagées sont :
18	18
	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	+
19	19	= Equipes =
20	20
21		- Les équipes impliquées, dont :
	58	+ 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
	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
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)
	64	+* Equipe VESONTIO, FEMTO-ST/DISC, Besançon
	65	+** (//à venir//) permanents impliqués dans le GT
	66	+** Représentant : Alain Giorgetti
29	29
	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	+
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.
	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/)