Fri 12 Jan 2018 16:15 - 16:40 at Bunker Hill - Synthesis Chair(s): Nadia Polikarpova

We describe algorithms for symbolic reasoning about executable models of type systems, supporting three queries intended for designers of type systems. First, we check for type soundness bugs and synthesize a counterexample program if such a bug is found. Second, we compare two versions of a type system, synthesizing a program accepted by one but rejected by the other. Third, we minimize the size of synthesized counterexample programs.

These algorithms symbolically evaluate typecheckers and interpreters, producing formulas that characterize the set of programs that fail or succeed in the typechecker and the interpreter. However, symbolically evaluating interpreters poses efficiency challenges, which are caused by having to merge execution paths of the various possible input programs. Our main contribution is the Bonsai tree, a novel symbolic representation of programs and program states which addresses these challenges. Bonsai trees encode complex syntactic information in terms of logical constraints, enabling more efficient merging.

We implement these algorithms in the BONSAI tool, an assistant for type system designers. We perform case studies on how BONSAI helps test and explore a variety of type systems. BONSAI efficiently synthesizes counterexamples for soundness bugs that have been inaccessible to automatic tools, and is the first automated tool to find a counterexample for the recently discovered Scala soundness bug SI-9633.

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

15:50 - 17:05
SynthesisResearch Papers at Bunker Hill
Chair(s): Nadia Polikarpova University of California, San Diego
15:50
25m
Talk
Strategy Synthesis for Linear Arithmetic Games
Research Papers
Azadeh Farzan University of Toronto, Zachary Kincaid Princeton University
16:15
25m
Talk
Bonsai: Synthesis-Based Reasoning for Type Systems
Research Papers
Kartik Chandra Stanford University, Rastislav Bodík University of Washington
16:40
25m
Talk
Program Synthesis using Abstraction Refinement
Research Papers
Xinyu Wang UT Austin, Işıl Dillig UT Austin, Rishabh Singh Microsoft Research