Skip to Main content Skip to Navigation
Theses

Preuves par induction implicite : cas des théories associatives-commutatives et observationnelles

Abstract : Automated induction proofs are a formal means for systems validation. In the framework of test set induction, we propose two automated proofs methods for conditional specifications: one deals with associative-commutative (AC) theories, the other with observational theories. In the first method, we give an algorithm for computing induction schemes, as well as a new inference system using elaborated AC rewriting techniques. For a class of specifications, the method detects non valid conjectures in a finite time. Interesting experiments on the correctness of digital circuits produced proofs requiring less interaction than other well-known provers. In the observational approach, data type objects are cnsidered as equal if they cannot be distinguished by experiments with observational results. These experiments are represented by particular terms called observable contexts. We propose an automated proof method of observational properties, relying on the computation of a finite set of well-chosen contexts called test contexts, that shematizes all the observable contexts. We also propose methods for computing such test contexts and a new inference system. For an interesting class of specifications, the method detects non observationally valid conjectures in a finite time.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_1997_0174_BEN_RAJEB.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01747440
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 11:00:03 AM
Last modification on : Friday, February 26, 2021 - 3:26:01 PM

Identifiers

  • HAL Id : tel-01747440, version 1

Collections

Citation

Narjes Ben Rajeb. Preuves par induction implicite : cas des théories associatives-commutatives et observationnelles. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1997. Français. ⟨NNT : 1997NAN10174⟩. ⟨tel-01747440⟩

Share

Metrics

Record views

14