* [Caml-list] [ANN] PROMELA library 0.4
@ 2012-09-03 17:22 Markus Weissmann
0 siblings, 0 replies; only message in thread
From: Markus Weissmann @ 2012-09-03 17:22 UTC (permalink / raw)
To: OCaml mailing list
Hi,
I'd like to announce version 0.4 of the PROMELA library. It provides types and functions to create, analyze and modify PROMELA programs as used by the Spin model checker.
The source code is available on ocamlforge under the new bsd license:
http://promela.forge.ocamlcore.org/
The purpose of the library is to make automated generation, rewriting and verification of PROMELA models easy. Think of it as something like "LLVM for model checking".
It comes with an example generator that can create a model of an arbitrary-sized dining philosophers problem.
Regards
-Markus
--
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2012-09-03 17:22 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2012-09-03 17:22 [Caml-list] [ANN] PROMELA library 0.4 Markus Weissmann
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox