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-... - A simple SQL-injection analyzer: https://hackage.haskell.org/package/sbv-7.7/docs/Documentation-SBV-Examples-... 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.