VERIMAG

Méthodes formelles et outils pour une informatique sûre et sécurisée, applications aux systèmes cyber-physiques

Les systèmes informatisés contrôlent de nombreux objets professionnels ou de la vie quotidienne, y compris ceux qui assurent des fonctions critiques dans le transport (automobile, avionique, ferroviaire, spatial), les télécommunications, les robots, le secteur bancaire ou celui de la santé, pour lesquels les attentes en matière de sécurité et de sûreté sont particulièrement fortes.

Les travaux de Verimag visent à produire des outils théoriques et techniques permettant de répondre à ces attentes avec une rigueur mathématique, sur un large spectre de problèmes pouvant porter sur des circuits, des processeurs, des systèmes analogiques ou hybrides, des compilateurs, des protocoles de sécurité, des algorithmes distribués, des systèmes intégrant de l’IA, en particulier dans le contexte des systèmes critiques. Verimag cherche à maintenir un équilibre entre recherche fondamentale, expérimentale et appliquée, en particulier grâce à des coopérations durables et soutenues avec des partenaires industriels et académiques.

Verimag a contribué et contribue activement au développement de l’état de l’art en méthodes formelles (model-checking, analyse statique, démonstration automatique ou interactive), langages synchrones, modélisation des systèmes, tout en intégrant les questions de durabilité et d’économie des ressources.

Les résultats de Verimag trouvent de nombreuses applications industrielles, notamment dans des outils pour le développement des logiciels et systèmes critiques.

Verimag (UMR 5104) a été créé en 1993 comme Unité Mixte CNRS/Verilog issu de l’équipe Spectre du laboratoire LGI ; depuis 1997, Verimag est une unité de recherche commune à l’Université Grenoble Alpes (y compris Grenoble INP-UGA) et au CNRS (INS2I).

Verimag joue un rôle important dans l’enseignement à l’Université Grenoble Alpes et à Grenoble-INP et dans la formation de doctorants.

Verimag participe à l’Institut Carnot LSI et au Labex PERSYVAL-Lab. Pour plus d’informations, consulter le dernier rapport d’activité ou l’évaluation qu’en a fait l’HCERES.

Mots clés : méthodes formelles : model checking, analyse statique, démonstration automatique et interactive, logique, modélisation, test - Systèmes critiques, embarqués, cyber-physiques - Sécurité et Sûreté - Langage Synchrone, Lustre - Compilation, compilation certifiée - Coq - Analyse temporelle - IA de confiance, IA explicable - robustesse des modèles d’apprentissage - Informatique frugale

Verimag
Bâtiment IMAG
Université Grenoble Alpes
150 place du torrent
38401 Saint Martin d’Hères
FRANCE
Phone : +33 4 57 42 22 42
Fax : +33 4 57 42 22 22

Directeur : David Monniaux