%%center
!!!Groupe de Travail sur la Vérification
%%

__News:__
Les [journées annuelles du GT-Verif|JA-2019] ont eu lieu les 17, 18 et 19 juin 2019 à Nantes, organisées par Benoît Delahaye et Didier Lime.
\\

Les [précédentes éditions|Journées Annuelles] ont eu lieu 
à [Verimag|http://www-verimag.imag.fr/?lang=fr] en 2018,
au [LACL|http://www.lacl.fr/fr/] en 2017,
à l'[IRIF|https://www.irif.univ-paris-diderot.fr/] en [2016|JA-2016],
au [LACL|http://www.lacl.fr/] (Créteil) en [2015|Journées annuelles 2015],
au [LIP6|http://www.lip6.fr/] (Paris) en [2014|Journées annuelles 2014] et au [LSV|http://www.lsv.ens-cachan.fr/] (Cachan) en [2013|Journées annuelles 2013].
%%

Le [GT Vérification|http://gt-verif.loria.fr/] est un groupe de travail du [GdR-IM|http://www.gdr-im.fr/].
\\
Des écoles d'été (ou d'hiver) sur le thème de la vérification sont [MOVEP|http://movep.lif.univ-mrs.fr/] et [VTSA|http://www.mpi-inf.mpg.de/vtsa13/].

!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)|http://cedric.cnam.fr/],
[CRIStAL|https://www.cristal.univ-lille.fr/], 
[Femto-ST (équipe VESONTIO)|http://www.femto-st.fr/],
[IBISC|http://www.ibisc.univ-evry.fr/],
[IRISA|http://www.irisa.fr/], 
[IRIF|https://www.irif.univ-paris-diderot.fr/],
[IRIT|http://www.irit.fr/],
[LAAS|http://www.laas.fr/],
[LACL|http://www.lacl.fr/fr/],
[Labri|http://www.labri.fr/],
[LIS|http://www.lis-lab.fr/], 
[LIFO|http://www.univ-orleans.fr/lifo/equipe.php?id=5],
[LIG|http://www.liglab.fr/],
[LIP|http://www.ens-lyon.fr/LIP/],
[LIP6|http://www.lip6.fr/], 
[LIPN|http://lipn.univ-paris13.fr/],
[LIX|http://www.lix.polytechnique.fr/], 
[LORIA|http://www.loria.fr/], 
[LS2N|https://www.ls2n.fr/],
[LSV|http://www.lsv.ens-cachan.fr/], 
[ONERA|http://www.onera.fr/],
[Verimag|http://www-verimag.imag.fr/] 
(cette liste n'étant ni exhaustive ni limitative).


%%block
!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.
%%
%%block
!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).
%%block
!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 ALGA|https://www.irif.fr/~serre/GT_ALGA/] du [GdR IM|http://www.gdr-im.fr/], et les [GT FORWAL|http://gdr-gpl.cnrs.fr/index.php?option=com_content&view=article&id=63&Itemid=62] (Formalismes et Outils pour la Vérification et la Validation) et [LTP|http://gdr-gpl.cnrs.fr/index.php?option=com_content&view=article&id=66:ltp&catid=38:statiques&Itemid=65] (Langages, Types et Preuves) du [GdR GPL|http://gdr-gpl.cnrs.fr/].

%%block
!Comité de pilotage
* Nathalie Bertrand, Inria, Irisa, Rennes (co-responsable)
* Véronique Cortier, CNRS, Loria, Nancy
* Benoit Delahaye, LS2N, Nantes
* Radu Iosif, VERIMAG, Grenoble
* Florent Kirchner, CEA, Gif-sur-Yvette
* Jérôme Leroux, CNRS, Labri, Bordeaux
* Mickael Randour, Université de Mons, Belgique
* Pierre-Alain Reynier, LIS, Marseille (co-responsable)
* Sylvain Schmitz, IRIF, Paris
* François Vernadat, CNRS, LAAS, Toulouse
%%
%%block
!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|http://people.rennes.inria.fr/Nathalie.Bertrand/] ou [Pierre-Alain Reynier|http://pageperso.lif.univ-mrs.fr/~pierre-alain.reynier/].
%%