Mon 16 Jan 2023 09:00 - 10:30 at Kenmore - Tutorials 3A
Mon 16 Jan 2023 11:00 - 12:30 at Kenmore - Tutorials 3B

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.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Tutorials 3ATutorialFest at Kenmore
09:00
90m
Tutorial
QuickChick: Combining Random Testing and Verification in Coq
TutorialFest
Leonidas Lampropoulos University of Maryland, College Park
11:00 - 12:30
Tutorials 3BTutorialFest at Kenmore
11:00
90m
Tutorial
QuickChick: Combining Random Testing and Verification in Coq
TutorialFest
Leonidas Lampropoulos University of Maryland, College Park