Groupe de Travail sur la Vérification#

News: Les prochaines journées annuelles du GT-Verif auront lieu les 16 et 17 juin 2016 à l'IRIF, Paris.

Les précédentes éditions ont eu lieu au LACL (Créteil) en 2015, au LIP6 (Paris) en 2014 et au LSV (Cachan) 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), IBISC, IRCCYN, IRISA, IRIF, IRIT, LAAS, Labri, LIF, LIFC, LIFL, LIFO, LIG, LIP, LIP6, LIPN, LIX, LORIA, 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 Jeux du GdR IM, 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, Irisa, Rennes
  • Thomas Brihaye, Université de Mons, Belgique
  • Véronique Cortier, Loria, Nancy
  • Benoit Delahaye, LINA, Nantes
  • Florent Kirchner, CEA, Gif-sur-Yvette
  • Jérôme Leroux, Labri, Bordeaux
  • Denis Lugiez, LIF, Marseille
  • Sylvain Schmitz, ENS Cachan
  • François Vernadat, LAAS-CNRS, Toulouse

Contact#

Pour faire partie de ce groupe de travail, il suffit de s'inscrire à la mailing-list. Pour cela, our pour des informations, envoyez un mail à Véronique Cortier.

Add new attachment

Only authorized users are allowed to upload new attachments.
« This page (revision-49) was last changed on 23-mars-2016 15:48 by Sylvain Schmitz