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

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
Testing and VerificationResearch Papers at Bunker Hill
Chair(s): Santosh Nagarakatte Rutgers University, USA
10:30
25m
Talk
Generating Good Generators for Inductive Relations
Research Papers
Leonidas Lampropoulos University of Pennsylvania, Zoe Paraskevopoulou Princeton University, Benjamin C. Pierce University of Pennsylvania
10:55
25m
Talk
Why is Random Testing Effective for Partition Tolerance Bugs?
Research Papers
Rupak Majumdar MPI-SWS, Filip Niksic MPI-SWS
11:20
25m
Talk
On Automatically Proving the Correctness of math.h Implementations
Research Papers
Wonyeol Lee Stanford University, Rahul Sharma Microsoft Research, Alex Aiken Stanford University
11:45
25m
Talk
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Research Papers
Shelly Grossman Tel Aviv University, Ittai Abraham VMWare Research, Guy Golan-Gueta VMWare Research, Yan Michalevsky Stanford University, Noam Rinetzky Tel Aviv University, Mooly Sagiv Tel Aviv University, Yoni Zohar Tel Aviv University