Projet de recherche

Les travaux effectués dans le cadre du projet RNTL Inka peuvent trouver de nombreux prolongement de recherches. Les contraintes présentent un potentiel important pour l'analyse de programme et font d'ailleurs l'objet de plusieurs recherches dans ce cadre. La mise au point d'un solveur de contraintes sur les flottants ouvre de nombreuses perspectives et je pense naturellement en exploiter un certain nombre. Les thèmes de recherche que j'envisage poursuivre sont les suivants :

• Détection automatique d'erreurs de programmation :
  Les programmes C contenant des expressions sur les flottants sont la source d'un certain nombre d'erreurs de programmation dont la détection n'est pas une tâche facile. De telles erreurs sont parfois causées par le comportement subtil des calculs sur les flottants. Par exemple, même lorsque $x \neq 0$, l'expression $x * x$ peut être égale à zero³ et être la cause d'une division par 0 (e.g. pour l'expression $1 / ( x * x )$). Les contraintes sur les flottants fournissent un cadre théorique et pratique clair pour traiter ces cas difficiles. Dans l'exemple précédent, l'utilisation d'une $FP-2B-consistance$ permet de savoir, à partir de la connaissance du domaine de définition de la variable $x$, si l'expression $x * x$ peut conduire ou non à un résultat égal à 0. Ces recherches auront donc pour objet de fournir un système de détection des erreurs potentielles d'un programme C faisant appel à des expressions sur les flottants. Si de tels systèmes existent déjà, ils laissent échapper des subtilités telles que celle de l'exemple précédent et il leur est particulièrement difficile de remonter d'une source d'erreur à sa cause, une caractéristique propre à la résolution de contraintes.

• Détection de non-conformité aux spécifications :
  La vérification de logiciel est aujourd'hui une voie de recherche importante qui utilise de nombreuses techniques allant de l'inspection et de la relecture des spécifications et du code à la preuve de propriétés en passant par des techniques de tests. Chacune de ces approches a montrer ses limites. Une voie complémentaire peut être ouverte en s'appuyant à la fois sur les recherches menées sur l'utilisation des contraintes dans l'analyse de programme (e.g. l'outil Inka) et sur celle menées sur l'utilisation des contraintes dans les spécifications (e.g. l'outil BZ-testing-tool). La confrontation de ces deux systèmes de contraintes ouvre de nouvelles possibilités. Une voie possible est la détection de non-conformités aux spécification d'un programme. Il s'agit de montrer qu'il existe des valeurs pour lesquelles le système de contraintes généré à partir du programme est insatisfiable alors que le système de contrainte généré à partir des spécifications est satisfiable pour ces même valeurs. Or, si la transformation de spécifications ou d'un programme en un système de contraintes est une technique aujourd'hui maîtrisée, l'utilisation des systèmes de contraintes produits pour la détection de non-conformités est un domaine aujourd'hui encore inexploré. L'un des problèmes soulevé concerne la confrontation de spécification de propriétés mathématique avec les expressions sur les flottants qui les implémentent. L'utilisation de solveurs sur les réels et de solveurs sur les flottants devraient apporter un certain nombre de réponses à cette question.

Si ces thèmes de recherche représentent le prolongement naturel de mes travaux actuels, je reste, comme j'ai pu le démontrer par le passé, ouvert à d'autre thèmes. Plus particulièrement, je pense pouvoir profiter avantageusement de mes diverses compétences pour travailler sur les langages pour les contraintes.