[SMT-LIB] Announcement: Embedding SMT solvers in Haskell

[Levent Erkok]

[This is an announcement regarding our recent work on leveraging the power of SMT solvers from within Haskell. We hope this work will be interesting to the subscribers of this mailing-list.]

For a while now, Galois has been interested in connecting automated solvers to our programming language of choice, Haskell, to make it possible to prove automatically some properties of our functions. We've made public two efforts out this week, as previews of what we're thinking in this space:

    * SBV: http://hackage.haskell.org/package/sbv
    * yices-painless: http://hackage.haskell.org/package/yices-painless

Both are EDSL's (embedded domain specific languages) for representing propositions to an SMT solver via Haskell functions and values. The idea is to be able to use SMT solvers directly within Haskell in a seamless way, where programmers need not even know that there is an underlying SMT solver doing the hard work. Users of these DSLs will be thinking/programming in terms of Haskell functions/values/idioms, while the library takes care of the interaction with the underlying solver, presenting a unified view of powerful SMT solving capabilities directly within the programming language.

Our efforts explore different parts of the design space for integrating SMT solvers within Haskell:

SBV (symbolic bit-vector) library takes advantage of QF_BV and QF_AUFBV solvers, adding symbolic bit-vectors to Haskell. It translates through SMT-Lib (Version 1 for the time being), and hence can be connected to arbitrary solvers. (However, Yices is the only solver we have hooked up so far.) The library supports symbolic signed/unsigned bit vectors, extensional arrays of symbolic values, and uninterpreted functions.

Yices-painless emphasizes a type-preserving translation from a minimal core language, taking advantage of Yices's C-API and integrating with Yices through Haskell's foreign-function interface. It supports bit vectors and uninterpreted functions. We have plans to move this library to use the SMT-lib interface as well, thus taking advantage of other solvers in the future.

Both EDSLs are ready for experimentation and feedback, and we welcome your comments.

More information is available on our company blog:

      http://corp.galois.com/blog/2011/1/18/merging-smt-solvers-and-programming-languages.html

Thanks,

Levent Erkok
Galois, Inc.