Micaela Mayero Homepage

Site du projet CerPAN.

L'objectif de ce projet est de développer et mettre en application des méthodes permettant de démontrer formellement la correction de programmes issus du domaine de l'analyse numérique. Le projet s'intéresse plus particulièrement à des programmes apparaissant de manière récurrente dans la résolution de problème critiques. Beaucoup de programmes critiques sont issus de cette science, mais les travaux traitant directement des applications des méthodes formelles aux programmes d'analyse numérique sont rares. La principale raison est l'utilisation intensive des nombres réels (à virgule flottante) dans les programmes numériques, alors que les méthodes formelles manipulent plutôt des nombres entiers, ou plus généralement des structures discètes.

Cependant, les outils de méthodes formelles et en particulier les systèmes de preuve formelle sont aujourd'hui de plus en plus adaptés pour que l'on s'intéresse à la famille des nombres réels (flottants, réels exacts), ce qui ouvre une brèche pour l'application de ces systèmes aux programmes d'analyse numérique. Deux méthodes sont explorées dans ce projet.
L'une consiste à utiliser des outils basés sur Why tels que Caduceus. Il s'agit de travailler sur un programme déjà existant, que l'on va annoter suivant les proprités que l'on souhaite voir préservées. Ces annotations génèrent alors des obligations de preuves pour divers systèmes de preuve formelle. Ces outils, développés par certains des membres de ce projet, ne traitent pas encore les nombres flottants. Une première phase de ce projet devra donc passer par l'extension de ces outils aux nombres flottants.

L'autre méthode consiste à effectuer la formalisation et la preuve du problème, puis à utiliser le principe d'extraction du système Coq afin d'obtenir automatiquement un programme prouvé correct. Ce principe d'extraction ne traite pas non plus encore la famille des nombres réels, et une autre phase de ce projet consistera à voir comment étendre l'extraction vers cette famille. Ces deux méthodes nécessitent la mise en place de techniques d'automatisation de preuves, afin de rendre nos méthodes accessibles aux programmeurs n'étant pas spécialistes des preuves formelles.

De manière annexe, nous essaierons de tenir compte des aspects d'efficacité qui peuvent jouer un rôle déterminant dans le domaine de l'analyse numérique en particulier. Les méthodes développées dans ce projet auront un champ large d'application dans les environnements destinés à produire du code numérique garanti correct par rapport àdes spécifications formelles. Le projet met en relation des membres dont l'expertise est diversifiée, pluridisciplinaire et adaptée aux objectifs (numériciens, experts en conception d'outils d'aide à la preuve, en preuves de programmes, en nombres réels et flottants) et pouvant justifier d'une certaine expérience dans ce domaine.