Sites Inria

English version

Prix ACM

17/06/2014

Coq reçoit le ACM Software System Award, prix prestigieux dans le domaine de l'informatique

De gauche à droite : Vinton Cerf, Brent Hailpern, Yves Bertot, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, John White (ACM Chief Executive Officer). - @ACM

Yves Bertot, responsable de l'équipe-projet Marelle Inria, sera invité le 21 juin prochain à San Francisco pour y recevoir le prestigieux prix Software System Award 2013, l'une des plus hautes distinctions de l’ACM (Association for Computing Machinery) qui est décernée le même jour que le Turing Award, aux côtés de Bruno Barras, Pierre Castéran, Thierry Coquand, Jean-Christophe Filliâtre, Hugo Herbelin, Gérard P. Huet, Chetan Murthy et Christine Paulin-Mohring, pour le développement du logiciel de preuve Coq, initialement baptisé COC pour Calculus of Inductive Constructions.  C'est la première fois depuis 40 ans qu'une équipe française reçoit ce prix, d'autant plus qu'elle a déjà été récompensée cette même année, lors de la conférence POPL 2014, par le prix ACM SIGPLAN Programming Languages Software Award. 

«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 est un des trois membres fondateurs du système Coq avec ses collègues d’Inria Gérard Huet et Thierry Coquand. 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 ».

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  ».

En avril 2004, Yves Bertot d' Inria et Pierre Castéran de l'Université de Bordeaux ont co-écrit le premier livre sur l'utilisation du système Coq :  "Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions" ; Ce livre fournit une introduction progressive aux concepts les plus novateurs du système Coq, en les décrivant à l'aide de nombreux exemples et exercices. Les problèmes les plus couramment rencontrés par les utilisateurs avancés du système sont également abordés et des solutions sont décrites. Ce livre, reconnu comme l'un des meilleurs livres sur le langage de programmation est très utilisé auprès des étudiants et enseignants.

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 :

- la certification au plus haut niveau des objectifs de sécurité d’une plateforme de carte à puce,

- le Théorème des 4 couleurs dont la démonstration complètement mécanisée a été terminée en 2004 par Georges Gonthier et Benjamin Werner 

- le Thèorème de Feit et Thompson dont la preuve du théorème a été terminée par Georges Gonthier et son équipe en septembre 2012.

- le compilateur CompCert C,  optimisant le langage C,  qui est entièrement programmé et prouvé en Coq.

Jusqu'à dernièrement, il a servi à détecter une faille dans le logiciel OpenSSL

 « 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.

Mots-clés : Coq ACM Software System Award

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !