[Haskell-cafe] [ANNOUNCE] New release of SBV (v7.7), now with symbolic characters and strings

[Levent Erkok]

I'm pleased to announce v7.7 release of SBV, a library integrating modern
SMT solvers into Haskell.

The main feature in this version is support for symbolic characters,
strings, and regular-expressions; initially contributed by Joel Burget. SBV
can now deal with proofs of programs that work on strings, taking advantage
of modern SMT solving techniques. This is the first time SBV is venturing
out of the realm of "number" like types (bit-vectors, reals, integers,
floats etc.), so I am excited about the new problem domains we can now
model symbolically.

A symbolic string is not a mere list of symbolic characters, but rather is
a type on its own. While this departure seems not in the spirit of Haskell,
this change of view brings a lot of expressive/proof power. Joel
contributed two simple examples to illustrate:

   - A regular-expression crossword solver:
   https://hackage.haskell.org/package/sbv-7.7/docs/Documentation-SBV-Examples-Strings-RegexCrossword.html
   - A simple SQL-injection analyzer:
   https://hackage.haskell.org/package/sbv-7.7/docs/Documentation-SBV-Examples-Strings-SQLInjection.html

Support for strings/regular-expressions is rather new in the SMT solving
arena. Furthermore, the logic is not known to be decidable, and thus the
solvers might struggle with difficult queries. Currently, only Z3 and CVC4
support this logic. If you do play with it, you're likely to find issues in
both SBV itself and possibly with the underlying solver as well. Please
report if you run into anything that looks fishy. In any case,
implementations are solid enough that you should be able to model and
reason about non-trivial string-processing programs with relative ease.


   -  Hackage: https://hackage.haskell.org/package/sbv
   -  Homepage: http://leventerkok.github.io/sbv/
   -  Release notes: https://github.com/LeventErkok/sbv/blob/master/
   CHANGES.md
   -  SMTLib initiative: http://smtlib.cs.uiowa.edu/


Thanks to Joel Burget for doing the initial work for adding support for
symbolic strings.

Feedback and bug reports are most welcome!

Happy reasoning!

-Levent.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180429/29823280/attachment.html>