A Certified Multi-prover Verification Condition Generator
Abstract
Deduction-based software verification tools have reached a maturity allowing them to be used in industrial context where a very high level of assurance is required. This raises the question of the level of confidence we can grant to the tools themselves. We present a certified implementation of a verification condition generator. An originality is its genericity with respect to the logical context, which allows us to produce proof obligations for a large class of theorem provers. This implementation is conducted within the Coq proof assistant, and is crafted so that it can be extracted into a standalone executable, independent of Coq, which is another originality.
Les outils de vérification de programme basés sur la preuve ont atteint un nouveau de maturité permettant leur utilisation dans un contexte industriel où un haut niveau de confiance est requis. Cela soulève la question du niveau de confiance que l'on peut mettre dans les outils eux-mêmes. Nous décrivons une implémentation certifiée d'un générateur d'obligations de preuve. Une originalité est sa généricité vis-à-vis du contexte logique, permettant de générer des obligations pour une grande famille de prouveurs. Cette implémentation est réalisée avec l'assistant à la preuve Coq, et est conçue dans l'optique d'en extraire un exécutable indépendant de Coq, garantit correct, ce qui est un autre originalité.
Origin : Files produced by the author(s)
Loading...