有界モデル検査（bounded model checking，BMC）は，システム（状態遷移系）と性質を述語論理式にエンコードし，その充足性をSAT/SMTソルバーで判定することにより，システムの安全性を示したり，不具合を見つけたりするための方法である．さまざまなBMCアルゴリズム（BMC法）が提案されているが，それぞれの方法は，実行パスのunrolling，実行パスに関する帰納法，状態の抽象表現など煩雑な考察に基づいて設計されている．BMC法の設計や実装にあたっては，背景の考察を理解して正確に行わなければ，検査器の信頼性が損なわれてしまう．そこで本研究では，高信頼なBMCツールの実現を目標に，BMC法および背景となる考察を証明支援系を用いて記述・検証し，さらに前記BMC法の記述をそのまま用いて検査を実施可能にする．具体的には，証明支援系Coq上にSheeranらが提案したBMC法を実装し，その健全性を証明し，プラグインされたSMTソルバーを利用して検査を実施可能にした．本研究の貢献は，(1) Sheeranらが提案した複数のBMC法とその健全性の証明をCoqで記述・形式化するとともに，一般的なBMC法へ流用可能な関数や定理を同定・整備したこと，(2)システム，性質，BMC法，その健全性の証明，SMTソルバーの入出力等をCoq上で記述し，検査対象システムの記述，システムの検査，BMC法の正しさの検証といった作業を統合したこと，の2点である．