Compilation C certifiée

Depuis 2003

D'abord dans le cadre de l'ARC Concert, puis 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.

Thèmes abordés

Dans le cadre de la thèse de Benoît Robillard, je m'intéresse également à une phase particulière de compilation, l'allocation de registres, ainsi qu'à la certification d'algorithmes d'optimisation combinatoire.

Concurrent Cminor

Depuis 2007
Avec Andrew W.Appel

Réutilisation de composants

2002-04

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.

Évaluation partielle

1990-2000

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.

On-going projects