|
 
|
[SD11] Automated Certification of Implicit Induction Proofs
Conférence Internationale avec comité de lecture : Certified Programs and Proofs, December 2011, Vol. 7086, pp.37-53, Series Lecture Notes in Computer Science, Kenting, Taiwan, (DOI: 10.1007/978-3-642-25379-9_5)
motcle:
Résumé:
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.
Collaboration:
LITA
BibTeX
| @inproceedings { | |||
| SD11, | |||
| title | = | "{Automated Certification of Implicit Induction Proofs}", | |
| author | = | " S. Stratulat and V. Demange ", | |
| booktitle | = | "{Certified Programs and Proofs}", | |
| year | = | 2011, | |
| month | = | "December", | |
| series | = | "Lecture Notes in Computer Science", | |
| volume | = | 7086, | |
| pages | = | "37-53", | |
| address | = | "Kenting, Taiwan", | |
| doi | = | "10.1007/978-3-642-25379-9_5", | |
| } | |||
