ポピュラーなモデル検査器。

これまたポピュラーなモデルチェッカー。

CSPを先祖にもつFSP記法がまあまあシンプルで好きです。Spinよりさくっと美しく書ける。規模が大きいとなるとSpinのが実用的かも。アップデートがJune 2006で止まっているけど、まあまあ使えるレベルまでいったということかもしれません。

シンガポール発の、モデル検査ツール（シミュレーションとかもできる）。CSPの拡張(グローバル変数相当もサポート)していて、実用的にしているようで興味深い。他にも確率、リアルタイム性に関する検証ができるようだ。