高階再帰スキームのモデル検査とそのプログラム検証への応用

前年度に引き続いた理論的な側面の研究と、そのプログラム検証への応用について研究を行った。1.ゲーム意味論と共通型理論の融合ゲーム意味論と共通型理論は、高階再帰スキームモデル検査問題への2つの主要なアプローチである。この2つのアプローチの関係を明らかにすることは未解決の課題であったが、我々は2つの結びつける理論(2レベルゲーム意味論)を構築することに成功した。また、この理論を応用することで既知のモデル検査アルゴリズムの計算量の新しい上界など、応用上有用な結果を与えた。2.ゲーム意味論に基づいた新しい高階再帰スキームモデル検査器ゲーム意味論に基づいた新しい高階再帰スキームモデル検査器を提案し、その評価を行った。まず、上で与えたゲーム意味論と共通型理論の対応関係を利用して、ゲーム意味論に基づく共通型の推論法を与えた。この推論法は一般には停止するとは限らないものであるが、この手法と抽象実行という技術を組み合わせることで必ず停止するアルゴリズムを得ることができる。高階再帰スキームのモデル検査は共通型の検査・推論に帰着できることが知られているため、得られた共通型推論器はモデル検査器として使うことができる。こうして得られたアルゴリズムが、特定の場合には既存の手法よりも優れていることを、実験的に確かめた。高階再帰スキームモデル検査はプログラム検証の際のボトルネックであり、この高速化はプログラム検証器の実用化にとって大変重要である。

前年度に引き続いた理論的な側面の研究と、そのプログラム検証への応用について研究を行った。1.ゲーム意味論と共通型理論の融合ゲーム意味論と共通型理論は、高階再帰スキームモデル検査問題への2つの主要なアプローチである。この2つのアプローチの関係を明らかにすることは未解決の課題であったが、我々は2つの結びつける理論(2レベルゲーム意味論)を構築することに成功した。また、この理論を応用することで既知のモデル検査アルゴリズムの計算量の新しい上界など、応用上有用な結果を与えた。2.ゲーム意味論に基づいた新しい高階再帰スキームモデル検査器ゲーム意味論に基づいた新しい高階再帰スキームモデル検査器を提案し、その評価を行った。まず、上で与えたゲーム意味論と共通型理論の対応関係を利用して、ゲーム意味論に基づく共通型の推論法を与えた。この推論法は一般には停止するとは限らないものであるが、この手法と抽象実行という技術を組み合わせることで必ず停止するアルゴリズムを得ることができる。高階再帰スキームのモデル検査は共通型の検査・推論に帰着できることが知られているため、得られた共通型推論器はモデル検査器として使うことができる。こうして得られたアルゴリズムが、特定の場合には既存の手法よりも優れていることを、実験的に確かめた。高階再帰スキームモデル検査はプログラム検証の際のボトルネックであり、この高速化はプログラム検証器の実用化にとって大変重要である。