[jhc] [ANNOUNCEMENT]Introducing scher, a symbolic testing library in the style of QuickCheck

Mario Alvarez Picallo mario.alvarez739 at gmail.com
Sat Jun 13 20:50:55 UTC 2015


Dear all,

I'm very pleased to announce that scher, the framework I've been working
on, has already reached the point where I feel I can present it to the
public and ask for feedback.

scher is a property-based testing framework for Haskell programs with a
similar API as QuickCheck or SmallCheck - the main difference is, instead
of random testing, it uses the Klee <http://klee.github.io/> engine to
perform concolic testing <https://en.wikipedia.org/wiki/Concolic_testing>,
a kind of SMT-enhanced testing which provides greater guarantees than
random testing.

If you want to get started with it, you will need:
* LLVM (I use version 2.9, but you should be able to get 3.4 working with
some effort)
* Klee
* The klee-uclibc <https://github.com/klee/klee-uclibc> library
* my fork of the jhc compiler <http://github.com/m-alvarez/jhc>, which adds
support for running code without a GC
* The scher <http://github.com/m-alvarez/scher> library
* The scher-run <http://github.com/m-alvarez/scher-run> program, which will
take care of feeding Klee the right input and formatting the output in a
human-readable format.

If anyone shows interest, I can write a quick-and-dirty tutorial of the
exact list of the incantations you need to get started.

As it is right now, everything is experimental and may be subject to
change. Furthermore, everything and anything may be broken. Feel free to
report any issues, bugs or simply feature requests on GitHub. Any feedback
is enormously helpful to me.

Happy verifying!

-- 
Now I do not know whether I was then a lambda expression emulating a Turing
machine, or whether I am a Turing machine emulating a lambda expression.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/jhc/attachments/20150613/1f53278a/attachment.html>


More information about the jhc mailing list