News
News: Les prochaines journées annuelles du GT-Vérif auront lieu à Lille, du 19 au 21 novembre, organisées par David Nowak et Vlad Rusu. Elles seront en partie conjointes avec les journées annuelles du GT SCALP.
Les précédentes éditions ont eu lieu à l’IRIF en 2023, au Labri en 2022, au LMF en 2021, au LS2N en 2019, à Verimag en 2018, au LACL en 2017, à l’IRIF en 2016, au LACL en 2015, au LIP6 en 2014 et au LSV en 2013.
Le GT Vérification est un groupe de travail du GdR-IM.
Des écoles d’été (ou d’hiver) sur le thème de la vérification sont MOVEP et VTSA.
Membres
La vérification est un thème de recherche étudié dans de nombreux laboratoires d’informatique en France, en particulier les laboratoires suivants : CEDRIC (CNAM), CRIStAL, Femto-ST (équipe VESONTIO), IBISC, IRISA, IRIF, IRIT, LAAS, LACL, Labri, LIS, LIFO, LIG, LIP, LIP6, LIPN, LIX, LORIA, LS2N, LSV, ONERA, Verimag (cette liste n’étant ni exhaustive ni limitative).
Contexte
Une des principales motivations de la vérification est l’analyse et la certification de codes critiques comme les codes embarqués (avions, satellites, fusées, automobiles), les systèmes répartis ou mobiles, les protocoles de sécurité (paiement sécurisé, authentification, vote électronique), ou plus généralement, tous les codes dont le bon fonctionnement est crucial d’un point de vue économique, médical ou sociétal. La vérification consiste à définir des modèles formels pour des systèmes informatiques et à mettre au point des algorithmes pour vérifier les propriétés de ces systèmes.
Thématiques
La vérification recouvre plusieurs aspects assez différents, qui pourront tous être étudiés au sein du GT Vérification.
- L’étude et la mise au point de modèles pour les systèmes informatiques (les automates à piles, à compteurs, temporisés, probabilistes, d’arbres, les systèmes de réécriture, les algèbres de calcul ou les systèmes de contraintes) et pour les propriétés des systèmes (logiques temporelles, logiques manipulant les données, les entiers, les pointeurs ou l’arithmétique). Suivant le contexte, ces logiques permettent l’étude de propriétés qualitatives ou quantitatives.
- Le model-checking, c’est-à-dire l’étude de la décidabilité et complexité de l’analyse de propriétés sur des systèmes de transitions et la mise au point d’algorithmes efficaces en pratique.
- Les techniques de preuves automatiques ou interactives (déduction automatique, prouveur du 1er ordre et ordres supérieurs, SAT-solveurs, procédures de décision en général) et la mise au point d’abstractions comme l’interprétation abstraite ou l’analyse statique pour raisonner sur des systèmes infinis.
- Le développement de modèles et techniques propres à la sécurité (analyse de protocoles de sécurité, vie privée, contrôle d’accès).
Lien avec les autres GT des GdR
Le GT Vérification a des thèmes de recherche qui recoupent en partie plusieurs autres GT existants comme le GT DAAL du GdR IFM, et les GT FORWAL (Formalismes et Outils pour la Vérification et la Validation) et LTP (Langages, Types et Preuves) du GdR GPL
Comité de pilotage
- Nathalie Bertrand, Inria, IRISA, Rennes (co-responsable)
- Silvano Dal Zilio, CNRS, LAAS, Toulouse
- Benoit Delahaye, LS2N, Nantes
- Jannick Dreier, CNRS, Loria, Nancy
- Radu Iosif, VERIMAG, Grenoble
- Jérôme Leroux, CNRS, Labri, Bordeaux
- Mickael Randour, Université de Mons, Belgique
- Pierre-Alain Reynier, LIS, Marseille (co-responsable)
- Sylvain Schmitz, IRIF, Paris
Contact
Pour faire partie de ce groupe de travail, il suffit de s’inscrire à la mailing-list. Pour cela, ou pour des informations, envoyez un mail à Nathalie Bertrand ou Pierre-Alain Reynier.