Test aléatoire et énumératif pour OCaml et Why3
1 : Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
Université de Franche-Comté, Ecole Nationale Supérieure de Mécanique et des Microtechniques, Centre National de la Recherche Scientifique : UMR6174, Université de Technologie de Belfort-Montbeliard : UMR6174
2 : CEA - List
CEA-LIST
3 : Laboratoire Méthodes Formelles
Université Paris-Saclay
4 : Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
Université de Franche-Comté, Ecole Nationale Supérieure de Mécanique et des Microtechniques, Centre National de la Recherche Scientifique : UMR6174, Université de Technologie de Belfort-Montbeliard : UMR6174
Nous présentons AutoCheck, un prototype d'outil de test aléatoire et énumératif de propriétés définies dans le langage fonctionnel OCaml ou dans le langage WhyML de la plateforme de vérification déductive Why3. Une originalité est que les tests énumératifs utilisent des générateurs de données eux-mêmes écrits dans le langage WhyML, et dont la correction et la complétude sont formellement prouvées avec Why3. Une autre spécificité est que l'effort de développement est réduit en exploitant le mécanisme d'extraction de Why3 vers OCaml et un outil de test aléatoire existant pour OCaml.
| Type : | : | oral |
| Thématiques | : | Session AFADL & MTV2 |
| PDF version | : |  PDF version |
- Poster
