1.1 定義と目的
プログラム検証とは、コンピュータプログラムが所定の仕様を満たすことを数学的・論理的手法によって厳密に証明する技術である。その目的は、ソフトウェアに潜むバグや脆弱性を開発段階で発見・排除し、プログラムの完全な正しさを担保することにある。テストやデバッグが実行時の挙動を部分的に確認する経験的手法であるのに対し、プログラム検証は形式的手法（フォーマルメソッド）に基づき、あらゆる入力条件下での動作を理論的に保証する。
1.2 歴史と発展
1.2.1 フロイドとホーアの貢献
1960年代、ロバート・フロイドはフローチャートを用いたプログラムの正当性証明の手法を提案した。その後、トニー・ホーアが「ホーア論理」を確立し、プログラムの事前条件と事後条件に基づく公理的意味論を打ち立てた。ホーア論理は、プログラムの部分的正しさを証明するための形式的枠組みとして広く受け入れられた。
1.2.2 モデル検査の登場
1980年代、エドマンド・クラーク、アレン・エマーソン、ジョセフ・シファキスらによってモデル検査が発明された。モデル検査は、有限状態システムの全状態空間を自動的に探索し、仕様を満たすかどうかを網羅的に検証する手法である。この画期的なアプローチは、ハードウェア検証や通信プロトコルの検証に革命をもたらし、2007年にクラークらはチューリング賞を受賞した。
1.3 検証の対象と限界
1.3.1 停止性問題と不完全性定理
プログラム検証には根本的な理論的限界が存在する。アラン・チューリングが示した停止性問題により、任意のプログラムが有限時間で停止するかどうかを判定する汎用アルゴリズムは存在しない。また、ゲーデルの不完全性定理は、十分に強力な形式的体系内で自身の無矛盾性を証明できないことを示している。これらの結果は、プログラム検証が原理的にすべての問題を解決できないことを意味する。
1.3.2 スケーラビリティの課題
現実の大規模ソフトウェアに対する検証の適用は、状態爆発問題や証明の複雑さによって制限される。プログラムのコード行数が増えるにつれて、検証に必要な計算資源や人間の労力が指数関数的に増大する傾向がある。このため、実用的な検証では部分的な検証や近似的手法が採用されることが多い。
2.1 ホーア論理
2.1.1 アサーションと事前条件・事後条件
ホーア論理では、プログラムの各部分に論理的な表明（アサーション）を付与する。事前条件はプログラム実行開始時に満たされるべき条件を記述し、事後条件は実行終了時に保証される条件を記述する。典型的なホーアトリプルは {P} S {Q} の形式で表され、「事前条件Pが成り立つ状態でプログラムSを実行すると、終了時に事後条件Qが成り立つ」ことを意味する。
2.1.2 部分正し性と完全正し性
部分的正し性（partial correctness）は、プログラムが停止する場合に事後条件が満たされることを保証する。一方、完全正し性（total correctness）は、プログラムが必ず停止することと、その結果として事後条件が満たされることの両方を要求する。完全正し性の証明には、プログラムの終了性を示すための整列順序を用いた証明が必要となる。
2.2 モデル検査
2.2.1 状態空間探索
モデル検査は、システムの取りうるすべての状態を有限状態遷移系としてモデル化し、その全状態空間を系統的に探索する。深さ優先探索や幅優先探索、シンボリックな状態表現などの技法を用いて、仕様違反が発生する状態や経路を自動的に発見する。
2.2.2 線形時相論理（LTL）と計算木論理（CTL）
モデル検査で使用される仕様記述言語として、線形時相論理（LTL）と計算木論理（CTL）が代表的である。LTLは単一の実行経路に沿った時間的性質（「常に」「いつか」「次に」など）を記述する。CTLは分岐する可能性のある計算木上の性質（「すべての経路で」「ある経路で」など）を表現する。これらの論理を用いて、安全性（悪いことは決して起こらない）や活性（良いことはいつか起こる）などの性質を検証する。
2.3 定理証明
2.3.1 自動定理証明と対話的定理証明
定理証明は、プログラムの正し性を数学的定理として定式化し、それを証明する手法である。自動定理証明はアルゴリズムによって完全に自動的に証明を試みるが、複雑な問題では困難な場合が多い。対話的定理証明では、人間の証明者がシステムと対話しながら証明を構築する。これにより、より複雑な証明が可能となる。
2.3.2 CoqとIsabelle/HOL
対話的定理証明器の代表的な実装として、CoqとIsabelle/HOLがある。Coqはフランス国立情報学自動制御研究所（INRIA）が開発した証明支援システムで、関数型プログラミング言語Gallinaと高階論理を統合している。Isabelle/HOLはケンブリッジ大学他が開発し、高階論理に基づく定理証明環境を提供する。両者ともコンパイラの検証や数学定理の形式化に実績がある。
2.4 抽象解釈
2.4.1 抽象領域と収束性
抽象解釈は、パトリック・クーザによって提唱された、プログラムの意味を抽象化して解析する手法である。具体的な値の集合を抽象領域（区間、多面体、符号など）に置き換え、計算の収束性を保証するために幅演算（widening）と縮小演算（narrowing）を用いる。これにより、無限の状態空間を有限の抽象表現で近似し、安全に解析することが可能となる。
2.4.2 静的解析への応用
抽象解釈は、静的コード解析ツールに広く応用されている。例えば、Astréeは航空宇宙分野のCプログラムに特化した静的解析器であり、抽象解釈を用いて実行時エラー（オーバーフロー、ゼロ除算、配列境界違反など）を検出する。抽象解釈による解析は、偽陽性と偽陰性のバランスを調整できる柔軟性を持つ。
3.1 主要なツール
3.1.1 SPIN
SPINは、ベル研究所のジェラルド・ホルツマンが開発したモデル検査ツールである。分散システムや通信プロトコルの検証に特化しており、PROMELAと呼ばれるモデル記述言語を使用する。SPINは線形時相論理（LTL）で記述された仕様を検証する高性能な探索エンジンを備えている。
3.1.2 NuSMV
NuSMVは、シンボリックモデル検査ツールであり、CTLおよびLTLの検証をサポートする。有限状態システムの記述言語SMVを用い、二分決定図（BDD）を用いたシンボリックな状態空間表現により効率的な検証を実現する。IRST（イタリア）とCMU（アメリカ）の共同プロジェクトとして開発された。
3.1.3 Frama-C
Frama-Cは、C言語のソースコードを対象とした静的解析プラットフォームである。ACSL（ANSI/ISO C Specification Language）を用いて仕様を記述し、ホーア論理に基づく検証条件生成、抽象解釈による静的解析、値解析などの多様なプラグインを統合している。産業利用も進んでおり、安全重要システムの検証に活用されている。
3.2 産業応用例
3.2.1 自動運転車の安全検証
自動運転車は、人命に関わるため厳格な安全保証が要求される。プログラム検証技術は、制御アルゴリズムやセンサフュージョン、経路計画などのモジュールに対して適用される。特に、ISO 26262などの機能安全規格への準拠を目的として、モデル検査や定理証明が利用される。実世界の複雑な運転シナリオを有限状態モデルに抽象化し、衝突回避などの安全特性を検証する試みが進められている。
3.2.2 スマートコントラクトの検証
ブロックチェーン上で動作するスマートコントラクトは、一度デプロイすると修正が困難であり、バグが存在すると甚大な経済的損失を引き起こす可能性がある。このため、イーサリアムのSolidity言語を対象とした検証ツールが多数開発されている。例えば、形式検証フレームワークKEVMは、Ethereum仮想マシンの完全な形式的意味論を提供し、スマートコントラクトの正し性を証明するために利用される。再入攻撃やオーバーフローなどの脆弱性を発見するために、シンボリック実行やモデル検査も応用されている。
3.3 検証プロセスの自動化
3.3.1 検証条件生成
検証条件生成（VCG）は、プログラムとその仕様から、証明すべき論理式（検証条件）を自動的に生成するプロセスである。ホーア論理の推論規則を適用し、プログラム構造に沿ってアサーションを伝播させる。生成された検証条件は、自動定理証明器やSMTソルバーに渡され、自動的または半自動的に証明される。
3.3.2 カウンター例を用いたデバッグ
検証プロセスにおいて、仕様が満たされないことが発見された場合、ツールは反例（カウンター例）を生成する。モデル検査では、仕様違反に至る具体的な実行経路が提示される。定理証明では、証明が失敗した位置や仮定の矛盾が示される。これらのカウンター例は、開発者がバグの原因を特定し、プログラムを修正するための強力な手がかりとなる。
4.1 大規模プログラムへの適用
4.1.1 モジュール化と合成検証
大規模プログラムの検証を実現するための重要な戦略として、モジュール化と合成検証がある。プログラムを独立したモジュールに分割し、各モジュールの振る舞いを契約（インターフェース仕様）として記述する。モジュールの内部実装が契約を満たすことを個別に証明し、契約の合成によって全体の正し性を保証する。この手法により、検証の複雑さをモジュール単位に分割し、スケーラビリティを向上させることができる。
4.1.2 確率的検証と近似手法
完全な形式的検証が困難な大規模システムに対して、確率的検証や近似手法が研究されている。確率的検証は、システムが確率的に振る舞うモデル（マルコフ連鎖など）を対象とし、仕様を満たす確率を計算する。近似手法では、抽象解釈や打ち切り探索などを用いて、ある程度の誤差を許容しながら検証結果を得る。これにより、完全な正しさが要求されない用途において実用的な検証が可能となる。
4.2 人間と機械の協調
4.2.1 証明支援システムの進化
対話的定理証明の分野では、より使いやすい証明支援システムの開発が進められている。証明の自動化レベルを高めるとともに、ユーザーインターフェースの改善、証明の可視化、ヒューリスティックな証明探索などの機能が追加されている。また、証明の再利用やライブラリの整備により、大規模な証明プロジェクトの生産性向上が図られている。
4.2.2 機械学習を用いた検証の効率化
機械学習技術をプログラム検証に応用する研究が活発に行われている。例えば、モデル検査の状態空間探索における優先順位付け、定理証明における補題の発見、検証条件の分類やヒューリスティックな意思決定などに深層学習が利用される。また、プログラムの潜在的なバグパターンを学習し、検証の前段階での絞り込みに活用する試みも進んでいる。
4.3 オープンな研究課題
4.3.1 複合システムの検証
今日のソフトウェアシステムは、ハードウェア、オペレーティングシステム、ネットワーク、データベースなど複数の層から構成される複合システムである。これらの異種システム間の相互作用や、タイミング制約、リソース制約などを形式モデルに取り込み、統合的に検証する手法の確立が課題となっている。特に、サイバーフィジカルシステム（CPS）やIoTシステムの検証が重要な研究対象である。
4.3.2 セキュリティとプライバシーの形式的保証
情報セキュリティとプライバシー保護に関する形式的保証は、ますます重要性を増している。情報フロー解析、非干渉性、暗号プロトコルの検証、プライバシー保護メカニズムの形式的証明などが研究されている。これらの分野では、攻撃者のモデル化や、計量情報の取り扱いなど、従来のプログラム検証とは異なる新たな理論的枠組みが必要とされている。