Please let me know what you find!<div>I may very well be putting some effort into an ltl Haskell model checker for work in the near future myself. <span></span><br><br>On Monday, November 16, 2015, Johannes Waldmann <<a href="mailto:johannes.waldmann@htwk-leipzig.de">johannes.waldmann@htwk-leipzig.de</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">For model checking concurrent and distributed imperative programs,<br>
there's the Promela language, and the Spin model checker<br>
( <a href="http://spinroot.com" target="_blank">http://spinroot.com</a> ) than can explore/enumerate<br>
a finite state space of a system and decide validity of LTL formulae.<br>
<br>
Is there something similar for Haskell models of concurrency?<br>
Ideally, some subset of Haskell (containing enough of<br>
Control.Concurrent.*) as an alternative for Promela.<br>
<br>
It should even be possible to put the model checking<br>
in an alternative implementation of respective monad<br>
(STM, IO for MVars) so the whole thing is an embedded DSL.<br>
<br>
somewhat related: this project is about a verified model checker:<br>
<a href="https://cava.in.tum.de/" target="_blank">https://cava.in.tum.de/</a> (ML code generated from Isabelle)<br>
but my interest is in model-checking concurrent programs<br>
in functional notation.<br>
<br>
- J.W.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="javascript:;" onclick="_e(event, 'cvml', 'Haskell-Cafe@haskell.org')">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>