TL;DR
ハードウェアやソフトウェアの設計から作ったモデルが、仕様を満たすかをアルゴリズムで調べる形式手法の 1 つ。仕様は時相論理の論理式で書くことが多い。
なぜ必要か
Wikipedia によると、モデル検査はもともと、離散的な状態を持つシステムの論理的な正しさを検査するために作られた。のちにリアルタイムシステムなどにも広がった。主な適用先はハードウェアの設計である。
仕組み
Wikipedia によると、プログラムは有限の状態遷移系に対応づけられ、状態をノード、遷移をエッジとする有向グラフで表される。モデル検査では、初期状態からのモデルで時相論理の式が成り立つかを判定する。モデルが有限なら、この判定はグラフの探索に帰着する。
状態爆発への対策
実際の問題では状態の数が膨大になる。これを状態爆発という。対策として、グラフを作らずに論理式で表す記号的な手法（二分決定図や SAT ソルバを使う）、結果に影響しない実行順序を省く半順序法、システムを単純化してから検証する抽象化がある。
例
代表的なツールに、SPIN、NuSMV、C/C++ 向けの CBMC、Java 向けの Java PathFinder、Alloy などがある。
注意点
Wikipedia によると、ソフトウェアには決定不能な問題が含まれるので、アルゴリズムだけでは証明も反証もできない場合がある。