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

Previous Topic Next Topic
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view

[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:
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.

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

Feedback and bug reports are most welcome!

Happy reasoning!


Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
Only members subscribed via the mailman list are allowed to post.