Certification des raisonnements formels portant sur des systèmes d'information critiques

Abstract : Proofs by induction are perfectly adequate to reasoning on unbounded data structures, for example naturals, lists and more generally on non-empty sets of elements provided with noetherian orders. They are largely used on different fields, particularly for the validation of properties of industrial applications in critical areas such as telecommunications and smart cards. The principle of noetherian induction is the basis of a set of modern techniques of proof by induction, including those based on implicit induction. In this thesis, we will focus on the integration of implicit induction reasoning like it is implemented by spike using the certified proof environnement Coq. Spike is an automatic theorem prover based on implicit induction that is capable of reasoning on conditional first-order theories. The implementation of Spike is not yet certified, even if the underlying theoretical foundations have been approved repeatedly by the scientific community. A suitable alternative is to certify only the proofs produced by Spike. In this case, the certification process must be automatic because scripts of Spike’s proofs are often long. Previous work has shown the possibility of certifying automatically some proofs by implicit induction generated by Spike using the certified environment provided by the Coq proof-assistant. We will propose new Coq tactics that are able to prove automatically theorems by implicit induction. Two approaches will be studied. The first approach consists on using Spike as an external tool. It is limited to process Coq specifications which can be translated in conditional specifications, as well as theorems convertible in conditional equations. Proofs generated by Spike are then translated into Coq scripts finally validated by its kernel. Another limitation is due to the translation of the application of a subset of the Spike inference rules. The second approche is to use strategies à la Spike to automatically build implicit induction proofs in Coq. This approach consists on creating tactics that perform like Spike inference rules to generate new subgoals in Coq. Comparing to the first approach, these tactics permit the use of Coq reasoning techniques which are not present in Spike and opens the possibility of mixing automatic and manual proof steps. Both approaches have been implemented and tested on several examples including lemmas used in the proof of validity of the conformity algorithm for the ABR telecommunications protocol
Document type :
Theses
Complete list of metadatas

Cited literature [73 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01751759
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 1:25:58 PM
Last modification on : Tuesday, April 10, 2018 - 1:26:58 AM

File

DDOC_T_2015_0082_HENAIEN.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01751759, version 1

Collections

Citation

Amira Henaien. Certification des raisonnements formels portant sur des systèmes d'information critiques. Autre [cs.OH]. Université de Lorraine, 2015. Français. ⟨NNT : 2015LORR0082⟩. ⟨tel-01751759⟩

Share

Metrics

Record views

552

Files downloads

110