L’importance prise par l’informatique dans notre quotidien nous contraint à faire confiance à des algorithmes et des systèmes informatiques pour des aspects de plus en plus cruciaux de notre vie. Que ce soit notre vie privée menacée par des attaques de plus en plus virulentes et sophistiquées contre des sites hébergeant nos données personnelles, ou des décisions nous concernant prises, en partie, par des algorithmes (par exemple, ParcoursSup pour l’orientation post-bac, ou des intelligences artificielles intervenant dans la détection de tumeurs), ou encore notre intégrité physique lors de déplacements dans des véhicules qui intègrent de plus en plus de logiciels de décision.

L’équipe MTV (Modèles et Technologies pour la Vérification) développe depuis de nombreuses années des techniques et des outils pour la sûreté de fonctionnement des systèmes informatiques. Notamment le langage AltaRica qui est désormais utilisé par plusieurs acteurs majeurs de l’industrie aéronautique pour la modélisation et la certification des avions. L’équipe MTV est également investie dans la preuve formelle du programme ParcoursSup d’orientation post-baccalauréat. Plus récemment, un partenariat s’est noué avec l’équipe “Progress” du LaBRI autour de “l'informatique de confiance”. Ce projet explore d’une part, le lien entre la preuve de programme et le test logiciel, ainsi que l’intégration de la preuve de programmes dans les pratiques de génie logiciel. Et d’autre part, la cyber-sécurité, avec l'objectif d'améliorer la robustesse des systèmes en tenant compte de la complexité des systèmes d’information actuels, en agrégeant les compétences issues de divers thèmes de recherche: systèmes d’exploitation, réseaux, simulation, intelligence artificielle, sûreté de fonctionnement, etc.