Automated Certification of Implicit Induction Proofs

Sorin Stratulat 1, 2 Vincent Demange 2
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Theorem proving is crucial for the formal validation of properties about user specifications. With the help of the Coq proof assistant, we show how to certify properties about conditional specifications that are proved using automated proof techniques like those employed by the Spike prover, a rewrite-based implicit induction proof system. The certification methodology is based on a new representation of the implicit induction proofs for which the underlying induction principle is an instance of Noetherian induction governed by an induction ordering over equalities. We propose improvements of the certification process and show that the certification time is reasonable even for industrial-size applications. As a case study, we automatically prove and certify more than 40% of the lemmas needed for the validation of a conformance algorithm for the ABR protocol.
Type de document :
Communication dans un congrès
Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. 2011
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00644876
Contributeur : Sorin Stratulat <>
Soumis le : vendredi 25 novembre 2011 - 14:20:04
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : lundi 5 décembre 2016 - 08:50:44

Fichier

document.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00644876, version 1

Collections

Citation

Sorin Stratulat, Vincent Demange. Automated Certification of Implicit Induction Proofs. Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. 2011. 〈hal-00644876〉

Partager

Métriques

Consultations de la notice

233

Téléchargements de fichiers

160