Parallélisation des systèmes de preuve interactifs de haute fiabilité – Paral-ITP

Les systèmes de preuve interactifs, et notamment ceux basés sur une
logique bien identifiée certifiée par un noyau bien circonscrit, ont
une importance croissante en informatique et en mathématiques, comme
purent en témoigner récemment la formalisation complète sur machine du
théorème des 4 couleurs ou la vérification semi-automatique d'un
compilateur C réaliste. Cependant, le développement de preuves de plus
en plus complexes exigent des capacités de calcul et d'interaction non
séquentiels de plus en plus importantes suggérant en autres
d'exploiter les opportunités de parallélisation offertes par les
architectures multi-cœurs des microprocesseur actuels.

Les architectures actuelles des systèmes de preuve interactifs tels
que Coq ou Isabelle (mais aussi HOL/HOL-Light) trouvent leur origine
dans le système précurseur LCF de 1979. Ces architectures garantissent
la correction logique des preuves, quelque soit le niveau de
complexité des méthodes utilisées, par le passage obligé à travers un
noyau logique réduit à l'API stable, bien délimitée et
mathématiquement bien comprise. Bien que Coq et Isabelle aient
considérablement étendu au fil des années leur puissance de preuve, la
richesse de leur langage de spécification et l'étendue de leurs
bibliothèques, le modèle opérationnel d'interaction avec le système
est resté essentiellement basé sur le principe de la boucle
d'interprétation séquentielle héritée de LCF.

Le projet que nous proposons a pour objectif de faire évoluer le
modèle d'interaction séquentielle de Coq et Isabelle en un modèle
d'interaction non linéaire permettant entre autres d'exploiter au
mieux les ressources des processeurs multi-cœurs actuels et d'offrir à
l'utilisateur plus de réactivité et plus de capacités de
traitement. Les opportunités pour paralléliser l'exécution de ces
systèmes se situent à différents niveaux : dans le noyau d'inférence
logique, dans la recherche de preuve, dans l'interprétation des
commandes, dans les interfaces utilisateurs. Néanmoins, ces extensions
conséquentes du modèle d'interaction des systèmes de preuve doivent
impérativement se faire en préservant à tout moment la cohérence
logique des théories mathématiques validées par ces systèmes.

Une fois l'architecture de Coq et Isabelle modifiée pour permettre le
traitement de tâches en parallèle, il devient possible de concevoir
une notion commune de modèle de document formel apte à combiner des
résultats provenant de requêtes asynchrones faites aux systèmes, tout
en maintenant un historique des changements effectués. Il est alors
possible d'interagir avec les systèmes au travers de cette notion de
modèle de document, soit pour la vérification en continu de
bibliothèques de preuves, soit pour une utilisation directe suivant le
principe des interfaces modernes Eclipse ou NetBeans.

Au final, notre objectif est de faire de Coq et Isabelle des outils
plus efficaces et plus ouverts avec une notion de modèle de document
et une technologie d'interface qui satisferont à la fois les
utilisateurs finaux et les développeurs d'extensions de ces deux
systèmes. De la sorte, c'est plusieurs décennies de recherche en
modélisation et preuve formelles qui deviendront accessibles à une
nouvelle échelle pour la construction d'outils de niveau de confiance
maximal dans le domaine des méthodes formelles.