Présentation
RÉSUMÉ
Un assistant de preuve est un logiciel interactif permettant à son utilisateur de construire des démonstrations de façon semi-automatique, tout en garantissant la correction de ces démonstrations. Ce type d'outil est utile à la vérification de logiciel critique. Cet article présente Coq, assistant de preuve développé en coordination avec l’Inria, à travers un exemple de vérification d'une fonction de tri. Ensuite sont décrits quelques domaines d'applications, notamment la sûreté du logiciel et la recherche en informatique et en mathématiques. Coq est considéré comme un des outils les plus fiables pour la validation du logiciel, ce qui s’explique par les fondements théoriques de cet outil et son évolution depuis plus de 30 ans de recherche et de développement.
Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.
Lire l'articleAUTEUR(S)
-
Sandrine Blazy : Université de Rennes 1, IRiSA, CNRS
-
Pierre Castéran : Univ. Bordeaux, LaBRI, CNRS, INP Bordeaux
-
Hugo Herbelin : Chercheur Inria Paris
INTRODUCTION
Face à l’importance croissante des composants informatiques – logiciels et matériels – dans des domaines critiques aussi divers que transports, énergie, santé, finance, etc., le besoin de composants sûrs se fait de plus en plus impérieux.
Par exemple, l’exécution d’un programme doit se faire sans erreur dans les conditions d’application prévues : absence d’erreur à l’exécution ou de bouclage non désiré, conformité à une spécification fonctionnelle.
Or nous savons, depuis Turing , qu’aucun algorithme ne peut automatiquement prendre en donnée un programme quelconque et rendre en un temps fini un diagnostic de correction. Par conséquent, seule une partie de la tâche de certification d’un logiciel peut être automatisée. Pour le reste, on peut recourir à des outils interactifs, où la preuve – souvent complexe – de correction doit être guidée par l’utilisateur.
Les assistants de preuve
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
MOTS-CLÉS
méthode formelle | assistant de preuve | logique | preuve de programme | logiciel certifié | Coq
DOI (DIGITAL OBJECT IDENTIFIER)
Coq, assistant de preuve
Exemple de développement en Coq : preuve de correction d’un algorithme simple
Sources bibliographiques
- (1) - - The CompCert compiler. http://compcert.inria.fr .
- (2) - - OCaml page.
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Article inclus dans l'offre
"Technologies logicielles Architectures des systèmes"
(
408 articles
)
Actualisée et enrichie d’articles validés par nos comités scientifiques.
Quiz, médias, tableaux, formules, vidéos, etc.
Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.
Un ensemble de services exclusifs en complément des ressources.
