Scala 2016
Sun 30 - Mon 31 October 2016 Amsterdam, Netherlands
co-located with SPLASH 2016
Mon 31 Oct 2016 14:45 - 15:10 at Matterhorn 2 - Analysis, Testing & Verification Chair(s): Philipp Haller

Bonsai is a tool that symbolically checks for soundness errors in type systems. It constructs a symbolic space of syntactically-correct programs and evaluates them on the actual typechecker and interpreter, looking for a program that passes the former but fails in the latter. Being a bounded model checker, Bonsai does not prove correctness of a type system, but it finds counterexamples twice as large as those found by experts. We demonstrate how to use Bonsai to find the recently-discovered Scala soundness issue SI-9633 (Amin & Tate), which is related to the interaction between null and path-dependent types.