| Popis: |
Un assistant de preuve est un logiciel interactif permettant a son utilisateur de construire des demonstrations de facon semi-automatique, tout en garantissant la correction de ces demonstrations. Ce type d'outil est particulierement utile a la verification de logiciel critique. Cet article presente Coq, assistant de preuve dont le developpement est coordonne par l'institut de recherche Inria. Son utilisation est d’abord presentee a travers un exemple tres simple: la verification d'une fonction de tri. Puis une deuxieme partie presente quelques domaines d'applications, notamment la surete du logiciel et la recherche en informatique et en mathematiques. Coq est considere comme un des outils les plus fiables pour la validation du logiciel, ce qui s’explique par les fondements theoriques de cet outil et son evolution depuis plus de 30 ans de recherche et de developpement. |
