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.
Conference DayMon 31 OctDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Mon 31 OctDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:10 | Analysis, Testing & VerificationScala at Matterhorn 2 Chair(s): Philipp HallerKTH 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évenartVrije Universiteit Brussel, Belgium, Jens NicolayVrije Universiteit Brussel, Belgium, Wolfgang De MeuterVrije Universiteit Brussel, Belgium, Coen De RooverVrije Universiteit Brussel, Belgium DOI | ||
14:45 25mTalk | Automatically finding Scala soundness bugs Scala Media Attached | ||