SMT-Based Checking of Predicate-Qualified Types for Scala
We present qualified types for Scala, a form of refinement types adapted to the Scala language. Qualified types allow users to refine base types and classes using predicate expressions. We implemented a type checker for qualified types that is embedded in Scala’s next-generation compiler Dotty and delegates constraint checking to an SMT solver. Our system supports many of Scala’s functional as well as its object-oriented constructs. To propagate user-provided qualifier ascriptions we utilize both Scala’s own type system and an incomplete, but effective qualifier inference algorithm. Our evaluation shows that for a series of examples exerting various of Scala’s language features, the additional compile-time overhead is manageable. By combining these features we show that one can verify essential safety properties such as static bounds-checks while retaining several of Scala’s advanced features.
Slides (scala16_schmid_slides.pdf) | 507KiB |
Mon 31 Oct Times are displayed in 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 - 13:55 Talk | SMT-Based Checking of Predicate-Qualified Types for Scala Scala DOI File Attached | ||
13:55 - 14:20 Talk | A Scala Library for Testing Student Assignments on Concurrent Programming Scala DOI File Attached | ||
14:20 - 14:45 Talk | 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 - 15:10 Talk | Automatically finding Scala soundness bugs Scala Media Attached |