Le monde numérique au service de la certification et de la sécurisation des systèmes 

Le logiciel coq récompensé

L'assistant à la preuve Coq vient d'être distingué par le prestigieux prix "ACM Software System Award", qui récompense une institution ou des individus pour le développement d'un système logiciel particulièrement influent par sa contribution conceptuelle et/ou son acceptabilité commerciale.



Coq est un logiciel permettant à la fois la production de programmes certifiés et la preuve de théorèmes mathématiques. De nombreux contributeurs ont participé à sa conception, sa réalisation et sa large diffusion. Une communauté de plus en plus large d'utilisateurs contribue à en établir de nouvelles applications.


Parmi les neuf récipiendaires explicitement nommés, figure Pierre Castéran, membre de l'équipe Méthodes Formelles du LaBRI, membre du cluster d'excellence CPU et co-auteur avec Yves Bertot du livre surnommé le Coq'Art, qui a largement contribué à la diffusion et l'enseignement de Coq sur plusieurs continents.


Nous sommes heureux de souligner que ce prix récompense une recherche collaborative menée sur une très longue durée, l'interaction entre théorie et programmation, et la synergie entre recherche et diffusion de la science.

Contact : pierre.casteran@labri.fr


Dernière mise à jour mercredi 23 avril 2014


HAUT