|
 
|
[BOI01] Prouveur Spécialisé pour le Langage d'Ensembles d'Entiers et de Booléens : LEEB
Conférence Nationale avec comité de lecture : AFADL'01, January 2001,
motcle:
Résumé:
Cet article donne un exemple d'automatisation des
preuves pour un sous-langage particulier de la
méthode B, en utilisant un prouveur dédié. Nous
définissons d'abord le langage, puis exposons la
stratégie de son prouveur associé, et son
implantation à l'aide de l'Atelier B. Nous
étudions ensuite ses propriétés. Un exemple réel
d'application industrielle est exposé pour
illustrer le processus.
BibTeX
| @inproceedings { | |||
| BOI01, | |||
| title | = | "{Prouveur Spécialisé pour le Langage d'Ensembles d'Entiers et de Booléens : LEEB}", | |
| author | = | " O. Boite ", | |
| booktitle | = | "{AFADL'01}", | |
| year | = | 2001, | |
| month | = | "January", | |
| } | |||
