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

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