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 OctDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 31 Oct
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:10 | Analysis, Testing & VerificationScala at Matterhorn 2 Chair(s): Philipp Haller KTH Royal Institute of Technology | ||
13:30 25mTalk | SMT-Based Checking of Predicate-Qualified Types for Scala Scala DOI File Attached | ||
13:55 25mTalk | A Scala Library for Testing Student Assignments on Concurrent Programming Scala DOI File Attached | ||
14:20 25mTalk | Building a Modular Static Analysis Framework in Scala (Tool Paper) Scala Quentin Stiévenart Vrije Universiteit Brussel, Belgium, Jens Nicolay Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel, Belgium, Coen De Roover Vrije Universiteit Brussel, Belgium DOI | ||
14:45 25mTalk | Automatically finding Scala soundness bugs Scala Media Attached | ||