GT VERIF

L’objectif de la vérification est l’analyse et la certification de codes
critiques comme les codes embarqués, les systèmes répartis ou mobiles, les
protocoles de sécurité, 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.

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
et pour les propriétés des systèmes. 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 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é.