[Haskell-cafe] model checking for (subset of) concurrent Haskell?
carter.schonwald at gmail.com
Tue Nov 17 01:16:29 UTC 2015
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe