Foundational Property-Based Testing - Archive ouverte HAL Access content directly
Conference Papers Year : 2015

Foundational Property-Based Testing

(1, 2) , (2) , (3) , (4) , (4)


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.
Fichier principal
Vignette du fichier
main.pdf (358.22 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01162898 , version 1 (11-06-2015)



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. ⟨10.1007/978-3-319-22102-1_22⟩. ⟨hal-01162898⟩
407 View
1208 Download



Gmail Facebook Twitter LinkedIn More