[Haskell-cafe] model checking for (subset of) concurrent Haskell?

[Carter Schonwald]

Please let me know what you find!
I may very well be putting some effort into an ltl Haskell model checker
for work in the near future myself.

On Monday, November 16, 2015, Johannes Waldmann <
johannes.waldmann at htwk-leipzig.de> wrote:

> For model checking concurrent and distributed imperative programs,
> there's the Promela language, and the Spin model checker
> ( http://spinroot.com ) than can explore/enumerate
> a finite state space of a system and decide validity of LTL formulae.
>
> Is there something similar for Haskell models of concurrency?
> Ideally, some subset of Haskell (containing enough of
> Control.Concurrent.*) as an alternative for Promela.
>
> 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.
>
> somewhat related: this project is about a verified model checker:
> https://cava.in.tum.de/ (ML code generated from Isabelle)
> but my interest is in model-checking concurrent programs
> in functional notation.
>
> - J.W.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org <javascript:;>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20151116/688ba3a7/attachment.html>