Hi Johannes, I released an initial version of a tool for the systematic testing of concurrent Haskell programs a couple of months ago[1]. I've never been quite certain where the boundary between model checking and testing is, but I think it's fair to say that what I've got is a bounded model checker. I presented a paper on it at the Haskell Symposium this year[2][3], but since then it has been improved significantly, both in terms of the concurrency features supported, and performance. The version on Hackage is very outdated now, but I hope to get a new release out reasonably soon.

Is there something similar for Haskell models of concurrency? Ideally, some subset of Haskell (containing enough of Control.Concurrent.*) as an alternative for Promela.

I didn't go for LTL, rather a more unit test-like approach[4] where you examine the final output of the program.

It should even be possible to put the model checking in an alternative implementation of respective monad (STM, IO for MVars) so the whole thing is an embedded DSL.

My approach is based on a typeclass abstraction, with a class for concurrency[5] and a class for STM[6]. Naturally, this means you can just write some Haskell polymorphic in the monad but constrained by the class, and then either run it "for real" using IO or STM, or test it using the testing instances. The current developmental version is on GitHub[7], and I'm writing up a technical report on it (draft online[8]). [1] https://hackage.haskell.org/package/dejafu [2] http://www.barrucadu.co.uk/publications/dejafu-hs15.pdf [3] https://youtu.be/jQCDa6WoFeY?list=PLnqUlCo055hV5dPC-4VWeXzhI8ooeTsVy [4] http://barrucadu.github.io/dejafu/Test-DejaFu.html [5] http://barrucadu.github.io/dejafu/Control-Monad-Conc-Class.html [6] http://barrucadu.github.io/dejafu/Control-Monad-STM-Class.html [7] https://github.com/barrucadu/dejafu [8] http://misc.barrucadu.co.uk/pub/techreport.pdf -- Michael Walker (http://www.barrucadu.co.uk)