2. Applications principales
L’exemple précédent pourrait laisser penser que Coq sert surtout à valider des programmes fonctionnels simples. Il n’en est rien. Des outils de vérification pour les langages dominants comme C, Java, Ada s’appuient totalement ou plus indirectement sur des bibliothèques écrites en Coq. Ces outils s’appuient sur la formalisation mathématique de la sémantique du langage de programmation considéré. Les théorèmes prouvés une fois pour toutes en Coq garantissent, soit la conformité de l’exécutable au source, soit des propriétés telles que l’absence d’erreurs à l’exécution, le déréférencement de pointeurs nuls, ou autres erreurs arithmétiques.
Sans être exhaustifs, nous pouvons citer quelques domaines d’application de Coq :
preuves de protocoles cryptographiques ;
analyse d’algorithmes distribués ;...
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Applications principales
Coq et sa place en informatique
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.
