Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Thu 22 Aug 2019 15:20 - 15:50 at Aurora Borealis - Paper Session 3: SMT & Arity Chair(s): Eric Seidel

Satisfiability modulo theories (SMT) solvers give programmers a useful interface to solve challenging constraints at runtime. SMT solving has been used for a vast variety of different, useful applications, ranging from strengthening Haskell’s type system to verifying network protocols.

Unfortunately, interacting with SMT solvers directly from Haskell requires a great deal of manual effort. Data must be represented in and translated between two forms: that understood by Haskell, and that understood by the SMT solver. As such a translation is often done via printing and parsing text, any notion of type safety is lost. Furthermore, direct translations are rarely sufficient, as it typically takes many iterations on a design in order to get optimal – or even acceptable – performance from an SMT solver on large scale problems. This need for iteration complicates the translation issue: it is easy and frustrating to introduce a runtime bug.

To address these problems, we introduce a new library, G2Q. G2Q includes a quasiquoter that allows solving constraints written in Haskell itself, thus unifying data representation, ensuring correct typing, and simplifying iteration. We describe the API to our library and its backend, which is based on the G2 symbolic execution engine. Finally, we demonstrate the usability of G2Q via four example programs.

Thu 22 Aug

haskellsymp-2019-papers
15:20 - 16:30: Haskell 2019 - Paper Session 3: SMT & Arity at Aurora Borealis
Chair(s): Eric SeidelBloomberg LP
haskellsymp-2019-papers15:20 - 15:50
Research paper
William T. HallahanYale University, Anton XueYale University, Ruzica PiskacYale University, USA
haskellsymp-2019-papers15:50 - 16:20
Talk
Paul DownenUniversity of Oregon, USA, Zachary Sullivan, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK