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@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@haskell.org javascript:; http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe