While verification in the Coq proof assistant is often described as “playing a video game”, that video game is only fun when what you’re trying to prove is true. Otherwise, it is an exercise in frustration, realizing deep into a proof that there is an error in your program wasting valuable time and effort. In this tutorial we will present QuickChick, a property-based random testing tool for Coq which can help uncover bugs early on in the design process. We will give an overview of QuickChick’s functionality with a special focus on the new automation features: how to effortlessly derive effective generators for random inputs satisfying complex constraints in the form of inductive relations, as well as partial decision procedures for such relations, allowing users to automatically test complex propositions.
Program Display Configuration
Mon 16 Jan
Displayed time zone: Eastern Time (US & Canada)change