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
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

13:30 - 15:00: Scala 2017 - Compilation at Regency C
Chair(s): Paolo G. GiarrussoUniversity of Tübingen, Germany
scala-2017-papers13:30 - 14:00
scala-2017-papers14:00 - 14:30
Aleksandar ProkopecOracle Labs, David LeopoldsederJohannes Kepler University Linz, Gilles DuboscqOracle Labs, Thomas WuerthingerOracle Labs
scala-2017-papers14:30 - 15:00
Franck CassezMacquarie University, Australia, Anthony SloaneMacquarie University