Libdmc

Libdmc ^{[ 1 ] [ 2 ]}は、 LIP6 ^{[ 3 ]}研究所で設計されたライブラリです。その目的は、既存のモデルチェッカーの配布を容易にすることです。また、 C++言語のおかげで、パフォーマンスを犠牲にすることなく、最も汎用的なインターフェースを提供するように設計されています。

モデル検査は、特性を検証することで、モデル化されたシステムの動作が正しいことを自動的に証明する方法を提供する。しかし、メモリを大量に消費するため、いわゆる状態空間爆発問題に悩まされる。この問題を克服するために多くの解決策が提案されている（例えば、 BDDのような決定図を用いた記号表現など）が、これらの方法はすぐに許容できないほどの時間を消費することになる。

分散型モデル検査は、専用クラスタの集約されたリソースを利用することで、メモリと時間の消費の両方を克服する方法です。しかし、モデルチェッカー全体を書き直すのは困難な作業であるため、libdmc のアプローチは、モデルチェッカーを構築するためのフレームワークを提供することです。