Foundational Property-Based Testing

Abstract : Integrating property-based testing with a proof assistant creates an interesting opportunity: reusable or tricky testing code can be formally verified using the proof assistant itself. In this work we introduce a novel methodology for formally verified property-based testing and implement it as a foundational verification framework for QuickChick, a port of QuickCheck to Coq. Our framework enables one to verify that the executable testing code is testing the right Coq property. To make verification tractable, we provide a systematic way for reasoning about the set of outcomes a random data generator can produce with non-zero probability, while abstracting away from the actual probabilities. Our framework is firmly grounded in a fully verified implementation of QuickChick itself, using the same underlying verification methodology. We also apply this methodology to a complex case study on testing an information-flow control abstract machine, demonstrating that our verification methodology is modular and scalable and that it requires minimal changes to existing code.
Type de document :
Communication dans un congrès
ITP 2015 - 6th conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. Springer, 9236, 2015, Lecture Notes in Computer Science. <10.1007/978-3-319-22102-1_22>
Liste complète des métadonnées

https://hal.inria.fr/hal-01162898
Contributeur : Maxime Dénès <>
Soumis le : jeudi 11 juin 2015 - 15:49:18
Dernière modification le : vendredi 17 février 2017 - 16:15:18

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos, Benjamin C. Pierce. Foundational Property-Based Testing. ITP 2015 - 6th conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. Springer, 9236, 2015, Lecture Notes in Computer Science. <10.1007/978-3-319-22102-1_22>. <hal-01162898>

Partager

Métriques

Consultations de
la notice

262

Téléchargements du document

486