D'abord dans le cadre de l'ARC Concert, puis actuellement dans le cadre du projet Compcert, je m'intéresse à l'utilisation des méthodes formelles pour spécifier et certifier un compilateur C, à l'aide de l'assistant à la preuve Coq. Cela nécessite de définir à différents niveaux d'abstraction des sémantiques formelles des langages du compilateur, et de prouver ensuite sur machine des propriétés de correction de ces sémantiques.

Avec Andrew W.Appel

Nous nous sommes intéressées à la réutilisation dans les phases amont du processus de développement de logiciels. Nous avons défini différents mécanismes de réutilisation de composants de spécifications formelles. Certains de ces mécanismes ont été spécifiés en B et implémentés en OCaml. Afin d'appliquer ces mécanismes à un domaine particulier, nous nous sommes également intéressées à des transformations de programmes SQL effectuant des mises à jour de bases de données. Ces transformations ont pour but de faire de la rétro-ingéniérie de programmes, afin de déduire des spécifications en B.

J'ai spécifié en sémantique naturelle et implémenté dans l'environnement Centaur, des transformations de programmes dédiées à la compréhension d'applications scientifiques industrielles écrites en Fortran. Ces transformations sont inspirées de l'évaluation partielle, qui a surtout été utilisée pour produire du code efficace. Les spécifications ont été écrites à un faible niveau d'abstraction, l'objectif étant de générer automatiquement un prototype en Prolog implémentant ces spécifications. La propriété selon laquelle ces transformations préservent la sémantique de Fortran a été prouvée sur papier seulement.