POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 14:20 - 14:45 at Amphitheater 44 - Probabilistic Programming Chair(s): Marco Gaboardi

Property-based random testing in the style of QuickCheck demands efficient generators for well-distributed random data satisfying complex logical predicates, but writing these generators can be difficult and error prone. We propose a better alternative: a domain-specific language in which generators are expressed by decorating predicates with lightweight annotations to control both the distribution of generated values as well as the amount of constraint solving that happens before each variable is instantiated. This language, called Luck, makes generators easier to write, read, and maintain.

We give Luck a formal semantics and prove several fundamental properties, including the soundness and completeness of random generation with respect to a standard predicate semantics. We evaluate Luck on common examples from the property-based testing literature and on two significant case studies; we show that it can be used in complex domains with comparable bug-finding effectiveness and a significant reduction in testing code size, compared to handwritten generators.

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00: Probabilistic ProgrammingPOPL at Amphitheater 44
Chair(s): Marco GaboardiSUNY Buffalo, USA
14:20 - 14:45
Talk
Beginner's Luck: A Language for Property-Based Generators
POPL
Leonidas LampropoulosUniversity of Pennsylvania, Diane Gallois-WongInria Paris, ENS Paris, Cătălin HriţcuInria Paris, John HughesChalmers University of Technology, Benjamin C. PierceUniversity of Pennsylvania, Li-yao XiaENS Paris
Pre-print
14:45 - 15:10
Talk
Exact Bayesian Inference by Symbolic Disintegration
POPL
Chung-chieh ShanIndiana University, USA, Norman Ramsey
Pre-print
15:10 - 15:35
Talk
Stochastic Invariants for Probabilistic Termination
POPL
Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria, Djordje ZikelicUniversity of Cambridge
15:35 - 16:00
Talk
Coupling proofs are probabilistic product programs
POPL