Sujet de thèse en informatique 2002
Duong Nguyen Que
Utilisation sûre et générique de prouveurs en
compilation
L’équipe d’analyse, de
transformation et d’instrumentation de programmes du Centre de Recherche en
Informatique (CRI) de l’École des mines de Paris a utilisé des algorithmes
manipulant des contraintes affines comme système de preuve pour obtenir
automatiquement le résultat d’une analyse, pour prouver la correction d’une
transformation de programme ou pour générer un code équivalent à une
spécification.
Deux types de problèmes se
posent lors de l’utilisation d’un tel système: les complexités en temps, espace
et magnitude d’une part, et l’adéquation des modélisations sous forme de
contraintes affines aux objectifs d’analyse. L’explosion combinatoire d’une
seule preuve élémentaire parmi des milliers peut bloquer une analyse
automatique ou bien en multiplier le temps d’exécution par un facteur supérieur
à dix. L’inadéquation d’une modélisation et son remplacement peut avoir des
répercussions sur un volume de code trop important qu’une nouvelle analyse
puisse être implémentée.
Le CRI a développé un outil d’analyse,
de transformation et d’instrumentation de programme appelé PIPS et l’a utilisé
pour étudier de nombreux programmes de benchmarks publics et pour évaluer des
applications industrielles. L’implémentation existante et son utilisation
permettent d’évaluer l’ampleur des problèmes posés par l’utilisation d’un prouveur dans un contexte de compilation.
Le premier objet de cette thèse
est de proposer une interface sûre et générique entre un compilateur et un
système de preuve automatique. Cette interface doit permettre au compilateur de
gérer les débordements en temps, en espace et en magnitude. Cette interface, ou
éventuellement une interface de niveau plus élevé, doit permettre de changer le
système de preuve automatique sans modifier le compilateur.
Ces interfaces seront ensuite d’abord
utilisées pour permettre à PIPS d’exploiter sans incident un premier système de
preuve à base de contraintes affines.
La généricité sera ensuite
exploitée en utilisant d’autres prouveurs, tel l’Omega
librairie, et d’autres abstractions que les systèmes de contraintes affines,
telles que les unions de systèmes et/ou les différences de systèmes. L’intérêt
de ces extensions sera évalué sur des benchmarks et des applications
industrielles.
François
Irigoin
Centre
de recherche en informatique
École
des mines de Paris
35, rue Saint-Honoré
77305 Fontainebleau cedex
Tél: 01
64 69 48 48