| 研究概要 |
本研究では、ソフトウェアの安全性向上のため、ソフトウェアを実行前に検証するための研究を行っている.本年度は、以下の成果が得られた.
1.高階再帰スキームに基づく関数型プログラムの検証手法の拡張
前年度に,関数型プログラムのさまざまな検証問題が高階再帰スキームと呼ばれる無限木を記述するための文法のモデル検査の問題に還元できることを示したが,このプログラム検証方式には,(1)プログラムが単純型システムで型付けされなければならない,(2)整数やリストなどの無限集合上のデータを扱えないという欠点があった.本年度は,リストや木構造処理プログラムの検証を可能にするために,高階木トランスデューサの一種であるHMTPを導入し,その検証問題を高階再帰スキームのモデル検査の問題に還元する手法を考案した.また,これによって、より広範囲の関数型プログラムの検証を行うための道筋が得られた.
2.型理論に基づく高階再帰スキームのモデル検査アルゴリズムの構築と実装
上記1のプログラム検証手法のためには、高階再帰スキームのモデル検査のアルゴリズムが必要であるが,従来知られていたアルゴリズムは極めて効率の悪く,実用には耐えないものだった.それに対し,本研究では典型的な入力に対しては効率よく動作するモデル検査アルゴリズムを考案,実装し,その有効性を示した.
また,高階再帰スキームのモデル検査の計算量について,従来の結果よりも精密な結果を得た.例えば,高階再帰スキームの生成する木が様相μ計算の論理式で表される性質を満たすか否かの判定問題の計算量は,いくつかのパラメタが定数であるという仮定のもとで,高階再帰スキームのサイズに対して多項式時間であることを示した.
3.メモリの使用法の検証のための型理論
C言語のプログラムにおいてfreeとmallocが正しく使われていること(具体的には2重に解放がおきない、mallocされたメモリ領域はプログラム終了時までに解放されるなどの性質)を検査するための検証器を作成し,その有効性を示した.
|
