並行アルゴリズムを正しく記述することは困難です。一般的なテスト手法は、並行プログラムのコンテキストではあまり役に立ちません。並行プログラムの動作は予測不可能であり、また一部のバグは特定の環境 (例えば、特定のハードウェアのリラックスメモリモデル) でのみ現れるためです。

モデルチェックは、制御された環境でプログラムのさまざまな実行トレースを体系的に調べることで、並行プログラムのバグを発見するのに役立つ正式な検証手法です。

このプロジェクトでは、この問題に対処するために斬新な手法を開発し、並行プログラムのために既存のチェックツールの改善を試み、現実世界のソフトウェアプロジェクトで実地テストを実行します。