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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [40 references]  Display  Hide  Download
Contributor : Maxime Dénès <>
Submitted on : Thursday, June 11, 2015 - 3:49:18 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Tuesday, April 25, 2017 - 6:58:10 AM


Files produced by the author(s)



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⟩



Record views


Files downloads