Cet axe regroupe des mathématiciens et des informaticiens dont la vérification logicielle constitue un fil conducteur des activités, de ses fondements mathématiques (logique, automates, graphes, ordres  …) à une mise en oeuvre pratique (analyseurs de terminaison et non-terminaison, vérificateurs de correction partielle …)

Logique

Les recherches développées dans le cadre de ce thème concernent essentiellement  la logique catégorique et la théorie des topos, ainsi que l’étude du rôle de l’Axiome du choix dans diverses branches des mathématiques (et notamment en analyse fonctionnelle).

Mathématiques discrètes

Ce thème regroupe les recherches de l’équipe en mathématiques discrètes.
On y développe des travaux en théorie des graphes, en reconstruction et décomposition des structures relationnelles, en arithmétique et combinatoire (et en particulier on s’intéresse à la description de structures ou de nombres réels à l’aide d’automates), en théorie de l’ordre (on s’intéresse notamment à des questions de bonne fondation et de bel ordre).

Vérification logicielle

Les travaux menés dans ce thème concernent l’analyse de terminaison et de non-terminaison pour la programmation logique et les systèmes de réécriture de termes. On s’intéresse également à la correction partielle de programmes logiques. Dans ce cadre, on étudie les liens entre interprétation abstraite et preuves interactives de programmes.