Vérification formelle et assistants de preuve
La vérification formelle établit, par une preuve mathématique vérifiée par machine, qu'un logiciel répond à sa spécification ; les assistants de preuve sont les outils qui construisent et vérifient de telles preuves.
Definition
La vérification formelle est la construction d'une preuve rigoureuse, vérifiée par machine, qu'un système satisfait une spécification formelle, et un assistant de preuve est un logiciel qui aide un utilisateur à développer de telles preuves et à en vérifier mécaniquement la validité.
Scope
Ce sujet couvre la vérification déductive et la démonstration interactive de théorèmes : les assistants de preuve basés sur la théorie des types ou la logique d'ordre supérieur (tels que Coq, Isabelle, Lean et Agda), l'approche LCF de la preuve fiable, le fondement des propositions-comme-types, l'automatisation de la preuve et les tactiques, ainsi que les artefacts vérifiés emblématiques, y compris les compilateurs et les noyaux de systèmes d'exploitation.
Core questions
- Comment la correction fonctionnelle complète peut-elle être prouvée et vérifiée par machine ?
- Pourquoi les assistants de preuve sont-ils fiables, et qu'est-ce que la base de calcul de confiance ?
- Comment la correspondance de Curry-Howard relie-t-elle les preuves et les programmes ?
- Que faut-il pour vérifier des systèmes réels comme les compilateurs et les noyaux ?
Key theories
- Approche LCF de la preuve fiable
- L'Edinburgh LCF de Gordon, Milner et Wadsworth a introduit un petit noyau de preuve de confiance par lequel tous les théorèmes doivent passer, de sorte que même une automatisation complexe ne peut pas produire de preuves non valides.
- Compilateur vérifié (CompCert)
- CompCert de Leroy est un compilateur C prouvé correct dans un assistant de preuve, avec un théorème vérifié par machine selon lequel le code généré affine la sémantique du programme source.
- Noyau de système d'exploitation vérifié (seL4)
- Klein et ses collègues ont produit une preuve vérifiée par machine de la correction fonctionnelle pour le micro-noyau seL4, démontrant une vérification de bout en bout des logiciels système de bas niveau.
Clinical relevance
La vérification mécanisée offre le plus haut niveau d'assurance disponible pour les logiciels critiques, produisant des compilateurs, des noyaux et des bibliothèques cryptographiques avec des garanties prouvées plutôt qu'une confiance basée sur les tests. Les assistants de preuve sont également de plus en plus utilisés pour formaliser les mathématiques elles-mêmes.
History
La démonstration interactive de théorèmes a débuté avec Edinburgh LCF dans les années 1970, dont le métalangage ML et le noyau de confiance ont façonné les systèmes ultérieurs. Les assistants basés sur la théorie des types tels que Coq et Agda et les systèmes de logique d'ordre supérieur tels qu'Isabelle/HOL ont mûri au cours des décennies suivantes, culminant dans des artefacts vérifiés emblématiques : le compilateur CompCert (2009) et le noyau seL4 (2009).
Debates
- Coût de la vérification versus assurance obtenue
- La construction de preuves vérifiées par machine pour de grands systèmes demande un effort énorme, suscitant un débat sur les cas où la vérification complète est justifiée par rapport aux cas où des méthodes plus légères suffisent, et sur la mesure dans laquelle la preuve peut être automatisée.
Key figures
- Robin Milner
- Michael Gordon
- Xavier Leroy
- Gerwin Klein
- Robert Harper
Related topics
Seminal works
- gordon1979
- leroy2009
- klein2009
- harper2016
Frequently asked questions
- Qu'est-ce qu'un assistant de preuve ?
- Un assistant de preuve est un logiciel dans lequel un utilisateur construit des preuves formelles de manière interactive tandis que le système vérifie mécaniquement chaque étape, de sorte qu'une preuve achevée est fiable jusqu'à un petit noyau bien examiné.
- En quoi la vérification d'un programme diffère-t-elle de son test ?
- Le test vérifie le comportement sur des entrées sélectionnées et ne peut que révéler la présence de bogues, tandis que la vérification formelle prouve la correction pour toutes les entrées autorisées par la spécification, établissant l'absence des erreurs spécifiées.