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.

Mon 31 Oct
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:10: Scala - Analysis, Testing & Verification at Matterhorn 2
Chair(s): Philipp HallerKTH Royal Institute of Technology
scala-201613:30 - 13:55
Georg Stefan SchmidEPFL, Switzerland, Viktor KunčakEPFL, Switzerland
DOI File Attached
scala-201613:55 - 14:20
DOI File Attached
scala-201614:20 - 14:45
Quentin StiévenartVrije Universiteit Brussel, Belgium, Jens NicolayVrije Universiteit Brussel, Belgium, Wolfgang De MeuterVrije Universiteit Brussel, Belgium, Coen De RooverVrije Universiteit Brussel, Belgium
scala-201614:45 - 15:10
Kartik ChandraHenry M. Gunn High School, Rastislav BodikUniversity of Washington, USA
Media Attached