本解説記事では，論理式の充足可能性判定を利用したモデル検査について説明する．モデル検査とは，アルゴリズムやシステムの設計に対して，その状態空間を探索することで，与えられた性質が満たされるかどうかを判定する自動検証手法である．近年高速化が著しい充足可能性判定ツール(SATソルバやSMTソルバ)を用いることで，高速な検証が実現できる．本稿では，まずモデル検査や充足可能性判定について概説した後，プログラムのソースコードをモデル検査する手法について説明する．次に，より一般的なシステム記述を検証対象とした場合について，有界モデル検査と呼ばれる手法を紹介する．これは，初期状態からの有限の決められた回数の遷移による動作について検証を行う手法である．更に，この制約を取り除き，システムの全動作を対象とした検証を実現する手法について説明する．