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.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Dubois, Catherine; Giorgetti, Alain: Tests and proofs for custom data generators (2018)
- 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)