Projet ANR-11-INSE-0001 – Paral-ITP : Parallélisation des systèmes de preuve interactifs de haute fiabilité
Programme : Ingénierie Numérique et Sécurité (INS) 2011
Année de financement : 2011
Coordinateur du projet : Monsieur WOLFF Burkhart (UNIVERSITE DE PARIS XI [PARIS- SUD])
Partenaires : Inria Centre Saclay - Île-De-France; Types, Logique et Calcul; Inria Centre Paris - Rocquencourt; Laboratoire de Recherche en Informatique
Montant : 456431.0 euros
Date de début : 2011
Durée : 40 mois
Résumé : 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.