6. Conclusion
Les assistants de preuve tels que Coq rendent possible la production de logiciels sûrs malgré leur complexité. Il est bien clair que tout programme ne doit pas être formellement vérifié, mais le nombre d’applications devant être sûres justifie l’émergence d’un métier que nous pouvons appeler ingénierie de la preuve , qui nécessite des compétences à la fois en logique et en génie logiciel.
Parmi les divers assistants de preuve, Coq se distingue par sa fiabilité, une bibliothèque standard très fournie, et un grand nombre de tactiques de preuve interactive.
Sa complexité pourrait effrayer l’utilisateur novice, mais on peut remarquer que ce n’est pas Coq qui est trop compliqué, mais la preuve rigoureuse, notamment d’algorithmes et de programmes, qui nécessite des outils suffisamment complets....
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Conclusion
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.
