Foundational property-based testing. 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.
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Dubois, Catherine; Giorgetti, Alain; Genestier, Richard: Tests and proofs for enumerative combinatorics (2016)
- Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
- Paraskevopoulou, Zoe; Hriţcu, Cătălin; Dénès, Maxime; Lampropoulos, Leonidas; Pierce, Benjamin C.: Foundational property-based testing (2015)