近年、これまで人間が行っていた重大な仕事の多くがコンピュータシステムに任されるようになってきている。そのような重要なシステムの多くは並行・分散システムであり、そのようなシステムの誤りにより悲惨な事態が起こる可能性を防ぐため、並行プログラムの形式的な検証の重要性が増している。並行プログラムは逐次プログラムよりも本質的に複雑であるので、形式的な検証は容易ではなく、逐次プログラムの検証よりも一般的な技術が必要となる。この点で、定理証明器は並行プログラムの検証のための道具として特に適していると思われる。しかしながら、現在の定理証明器を並行プログラムの検証に直接適用することは困難である。なぜなら、並列性および非決定性のため、システムのとりうる状態数が爆発してしまうからである。また、定理証明器の多くには、λ計算に関して推論するための機構が備わっており、逐次プログラムの検証に利用することができるが、並行プログラムの検証のためのそのようなサポートはない。並行プログラムの検証をサポートするため、定理証明器上にプロセス計算を形式化した研究はあるが、それらは純粋なプロセス計算を対象としており、実用的なプログラムの検証を行う上では不十分である。

　本論文では、定理証明器を用いた現実的な並行プログラムの検証を可能にするための2つのアプローチを提案し、定理証明器Coqを用いて評価を行う。

　1番目のアプローチとして、並行プログラムを関数プログラムとしてモデル化、検証する手法を提案する。このアプローチでは、検証の対象とする並行プログラムおよびその環境をシステマティックに関数としてモデル化する。例えば、並行プログラムの非決定性は、関数の引数として試行オラクルを与えることによって表現される。このアプローチに基づき、現実的なクライアント／サーバアプリケーションの例として、SMTPサーバの受信部分(700行のJavaプログラム)が満たすべき4つの性質を形式的に検証した。この検証により、プログラムのバグを発見するとともに、証明の複雑さが適切な範囲内におさまることを確認した。このアプローチは、上記の利点にも関わらず、様々な問題を抱えている。例えば、モデルが複雑になり、補題の再利用性も落ちる。

　第2のアプローチでは、上記に述べた第1のアプローチの問題点を解決するために、並行プログラムを直接定理証明器上にモデル化し、検証するためのライブラリを設計、実装する。このライブラリは、(1)モデル記述言語、(2)仕様記述言語、(3)検証に利用する補題群からなる。モデル記述言語は、Coqのデータ型と関数を用いて拡張されたpi計算として構築される。仕様記述言語は、公平性の概念を導入して拡張された空間論理として構築される。これは、種々の現実的な並行プログラムをモデル化・定式化するのに役立つ。補題群の設計において、並行プログラムが多くの状態をもつ場合に状態空間が爆発するとい問題がある。我々は、partial order reduction ---検証のために探索される状態空間を削減する技術--- を我々の仕様記述言語の述語に適応することにより、この問題を解決した。このライブラリ(Coqのスクリプトでおよそ1万5 千行)を用いて、第1のアプローチで用いたメールサーバプログラムモデル化を行い、大事な性質を形式的に検証した。この実験により、複雑なモデル化の技術を用いることなく、現実的な並行プログラムを定理証明器上で検証できることを示した。

　本論文は、定理証明器を用いて現実的な並行プログラムの検証を可能にするための2つのアプローチを提案し、定理証明器Coqを用いてその評価を行っている。本論文は9章から成り、第1章は導入、第2章は準備である。第3章と第4章で1番目のアプローチについて述べ、第5章から第8章まで2番目にアプローチについて述べている。第9章は結論である。

　1番目のアプローチでは、並行プログラムを関数プログラムとしてモデル化し、定理証明器を用いて関数プログラムの検証を行う。第3章において関数プログラムによるモデル化の方法について述べられている。第4章では、このアプローチに基づき、現実的なクライアント／サーバアプリケーションの例として、SMTPサーバの受信部分の検証を行った事例について述べられている。SMTPサーバの受信部分（700行のJavaプログラム）が満たすべき4つの性質が定理証明器Coqを用いて形式的に検証された。この検証により、プログラムのバグを発見するとともに、証明の複雑さが適切な範囲内におさまることが確認された。

　第2のアプローチでは、並行プログラムを直接定理証明器上にモデル化し、以下のようなライブラリを用いて定理証明器上で検証を行う。ライブラリは、(1)モデル記述言語、(2)仕様記述言語、(3)検証に利用する補題群からなる。モデル記述言語は、Coqのデータ型と関数を用いて拡張されたπ計算として構築される。

　第5章では、まず、仕様記述言語とモデル記述言語が非形式的に導入される。そして、この枠組みのもとで、並行プログラムが多くの状態をもつ場合に状態空間が爆発するとい問題に対処するため、検証のために探索する状態空間を削減する技術であるpartial order reductionに必要な定理が証明されている。

　第6章では、モデル記述言語が定理証明器Coq上で形式化され、特に公平性の概念が形式的に定義されている。次の第7章では仕様記述言語が形式化され、並行プログラムの検証に必要な補題群が検証されるとともに、上述のpartial order reductionも公理化されている。仕様記述言語は公平性の概念を導入して拡張された空間論理として構築されており、種々の現実的な並行プログラムをモデル化・定式化するのに役立つと考えられる。

　最後に、第8章において、ライブラリ（Coqのスクリプトでおよそ1万5 千行）を用いて、第1のアプローチで用いたメールサーバプログラムのモデル化が再度行われ、その重要な性質が形式的に検証されている。この実験により、複雑なモデル化の技術を用いることなく、現実的な並行プログラムを定理証明器上で検証できることが示された。このアプローチは、第1のアプローチと異なり、並行プログラムを直接的にモデル化・検証することができるとともに、ライブラリによる検証の再利用性が高いという利点がある。

　結論として、以上の研究は、現実的な並行プログラムの形式的な検証技術にとって多大な貢献と考えられる。よって本論文は博士（情報理工学）の学位請求論文として合格と認められる。