Write a Blog >>
Scala 2017
Sun 22 - Mon 23 October 2017 Vancouver, Canada
co-located with SPLASH 2017
Sun 22 Oct 2017 14:30 - 15:00 at Regency C - Compilation Chair(s): Paolo G. Giarrusso

Satisfiability modulo theory (SMT) consists of determining the satisfiability of logical formulas. It can reason in various formal theories, e.g. in linear integer or real arithmetic, first-order logic, or logics of arrays. An SMT solver is a program that implements the corresponding algorithms to automatically determine whether a logical formula is satisfiable.

The SMTLIB initiative provides a common input and output format based on S-expressions for interacting with SMT solvers. We present ScalaSMT, a Scala library that provides an abstraction over the SMTLIB format. The library brings consistency and type safety to the textual and dynamically typed world of SMTLIB solver interaction.

ScalaSMT relies on the SMTLIB input/output capabilities of the solvers and consequently provides access to numerous popular SMTLIB-compliant solvers such as Z3,CVC4, Yices, MathSat5} or SMTinterpol.

ScalaSMT is easily extendable (SMTLIB commands and theories can be added) and configurable (SMTLIB-compliant solvers can be added). ScalaSMT fills a gap in the Scala library landscape by providing support for powerful logical reasoning algorithms.

Sun 22 Oct

Displayed time zone: Tijuana, Baja California change

13:30 - 15:00
CompilationScala 2017 at Regency C
Chair(s): Paolo G. Giarrusso University of Tübingen, Germany
13:30
30m
Talk
A Scala Framework for Supercompilation
Scala 2017
DOI
14:00
30m
Talk
Making Collection Operations Optimal with Aggressive JIT Compilation
Scala 2017
Aleksandar Prokopec Oracle Labs, David Leopoldseder Johannes Kepler University Linz, Gilles Duboscq Oracle Labs, Thomas Wuerthinger Oracle Labs
DOI
14:30
30m
Talk
ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)
Scala 2017
Franck Cassez Macquarie University, Australia, Anthony Sloane Macquarie University
DOI