Fri 12 Jan 2018 10:30 - 10:55 at Bunker Hill - Testing and Verification Chair(s): Santosh Nagarakatte

Property-based random testing (PBRT) is widely used in the functional programming and verification communities. For testing simple properties, PBRT tools such as QuickCheck can automatically generate random inputs of a given type. But for more complex properties, effective testing often demands generators for random inputs that belong to a given type and satisfy some logical condition. QuickCheck provides a library of combinators for building such generators by hand, but this can be tedious for simple conditions and error prone for more complex ones.
Fortunately, the process can often be automated. The most prominent method, narrowing, works by traversing the structure of the condition, lazily instantiating parts of the data structure as constraints involving them are met.

We show how to use ideas from narrowing to compile a large subclass of Coq’s inductive relations into efficient generators, avoiding the interpretive overhead of previous implementations. More importantly, the same compilation technique allows us to produce proof terms certifying that each derived generator is good—i.e., sound and complete with respect to the inductive relation it was derived from. We implement our algorithm as an extension of QuickChick, an existing tool for property-based testing in Coq. We evaluate our method by automatically deriving good generators for the majority of the specifications in Software Foundations, a formalized textbook on programming language foundations.

Fri 12 Jan (GMT-07:00) Tijuana, Baja California change

10:30 - 12:10: Research Papers - Testing and Verification at Bunker Hill
Chair(s): Santosh NagarakatteRutgers University, USA
POPL-2018-papers10:30 - 10:55
Leonidas LampropoulosUniversity of Pennsylvania, Zoe ParaskevopoulouPrinceton University, Benjamin C. PierceUniversity of Pennsylvania
POPL-2018-papers10:55 - 11:20
POPL-2018-papers11:20 - 11:45
Wonyeol LeeStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford University
POPL-2018-papers11:45 - 12:10
Shelly GrossmanTel Aviv University, Ittai AbrahamVMWare Research, Guy Golan-GuetaVMWare Research, Yan MichalevskyStanford University, Noam RinetzkyTel Aviv University, Mooly SagivTel Aviv University, Yoni ZoharTel Aviv University