Le logiciel Coq obtient deux prix internationaux

Par Gaëlle Degrez / Publié le 16 mai 2014

Le logiciel français Coq, dont une partie des développements ont été effectués au Laboratoire de Recherche Informatique de l’Université Paris-Sud, vient de se voir décerner deux prix prestigieux.

Ils sont neuf[1] à être invités le 21 juin prochain à San Francisco pour y recevoir le prestigieux prix Software System Award 2013, la plus haute distinction de l’ACM (Association for Computing Machinery) pour un logiciel. Et motif supplémentaire de satisfaction, ils sont les premiers français à être ainsi honorés, qui plus est déjà récompensés cette même année lors de la conférence POPL 2014 par le prix ACM  SIGPLAN Programming Languages Software Award. Ce qui leur vaut ces distinctions prestigieuses ? Le développement d’un logiciel de preuve Coq, initialement baptisé COC pour Calculus of Inductive Constructions.

Comment le prouver ?

«Coq est un assistant de preuve, c'est-à-dire qu’il fournit un langage et un environnement pour écrire des définitions et des preuves mathématiques » explique Christine Paulin-Mohring, professeur à l’Université Paris-Sud et membre de l’équipe de recherche TOCCATA, une équipe projet commune au Laboratoire de Recherche en Informatique (LRI) de l’Université Paris-Sud et à Inria. Christine Paulin, qui est un des trois membres fondateurs du système Coq avec ses collègues d’Inria G. Huet et T. Coquant, a présidé aux fondements mêmes du système en mettant au point les types inductifs qui sont un trait fondamental de Coq et qui en ont fait son succès. Dans un texte qu’elle a publié dans le numéro du mois de mai du bulletin de la société informatique de France, la chercheuse qui a par ailleurs largement participé au développement du système depuis ses premières versions, précise que la principale fonctionnalité de COQ est de « vérifier la correction des preuves, c’est un « relecteur » impartial et intraitable qui ne laisse passer aucune erreur ou omission dans un développement». Son collègue Jean-Christophe Filliâtre a rejoint l’équipe en 1994 pour son  DEA et a soutenu sa thèse en 1999. Il a notamment travaillé sur le code de Coq pour en refaire l'architecture, et plus spécifiquement  pour isoler la partie critique du système et ainsi garantir une plus grande sûreté (un détail qui a son importance, Coq étant lui-même utilisé pour certifier d'autres logiciels). Le chercheur note que l’efficacité du logiciel tient dans ce que « l’utilisateur interagit avec Coq pour introduire des définitions, énoncer des théorèmes et construire des preuves, le système vérifie alors la validité de ces différents éléments ».

Il a lui-même fait ses preuves

Fruit de près de 30 ans de développements et de multiples contributions, le logiciel Coq a été utilisé avec succès dans plusieurs contextes depuis la certification au plus haut niveau des objectifs de sécurité d’une plateforme de carte à puce jusqu’à la preuve du théorème des quatre couleurs. « Coq est un bel exemple de succès du modèle de recherche français qui a permis à un projet collaboratif de se développer sur le long terme » se félicitent ses auteurs.

[1] Bruno Barras, Yves Bertot, Pierre Castéran, Thierry Coquand, Jean-Christophe Filliâtre, Hugo Herbelin,  Gérard P. Huet, Chetan Murthy, Christine Paulin-Mohring.

 

Contacts : Christine Paulin-Mohring, Jean-Christophe Filliâtre – LRI (UPSud/CNRS) – christine.paulin @ lri.fr, jean-christophe.fillatre @ lri.fr

Le Théorème des quatre couleurs : La démonstration du théorème des quatre couleurs selon lequel toute carte planétaire peut être coloriée avec seulement quatre couleurs sans que deux pays ayant une frontière commune soient de la même couleur a tenu des générations de mathématiciens en haleine. Enoncé en 1852 par le mathématicien sud-africain Francis Guthrie, ce théorème n'a été démontré qu'à la fin des années 70. Cette preuve était cependant difficile à vérifier, car impliquant de très nombreux calculs. Le théorème des quatre couleurs a finalement pu être entièrement prouvé et vérifié à l'aide de Coq en 2006.


Carte de France en quatre couleurs / © Wikipédia

Dernière modification le 16 mai 2014