直接的モデル検査を用いた関数型プログラム検証手法

2017 Fiscal Year Annual Research Report

• Project/Area Number: 16J01038
• Research Institution: The University of Tokyo
• Principal Investigator: 寺尾 拓 東京大学, 情報理工学系研究科, 特別研究員(DC1)
• Project Period (FY): 2016-04-22 – 2019-03-31
• Keywords: プログラム検証 / 関数型プログラム / 高階モデル検査 / 述語抽象化 / 抽象解釈

Outline of Annual Research Achievements

Kobayashiらの高階モデル検査に基づく、関数型プログラム検証手法では、検証対象の関数型プログラムに含まれる整数型を、述語を用いて有限個の真偽値型のタプルとして表現する「述語抽象化」という過程にスケーラビリティ上のボトルネックが存在している。その原因は、抽象化の過程で発生する、SMTソルバの多数の呼び出しである。従来の手法では抽象化後にモデル検査を行うため、モデル検査を行えば到達しないとわかっている状態に対しても抽象化を行わざるをえず、無駄なSMTソルバの呼び出しが発生していた。
このボトルネックを改善するため、前年度に引き続き、述語抽象化とモデル検査を同時に行う融合アルゴリズムの改善、及びアルゴリズムの定式化とその正当性の証明を行った。また、定式化と証明をする過程で、抽象化前のプログラムの構文に基づき、抽象化後のプログラムの実行結果を表す、新たな抽象意味論を発見した。この意味論は上記の性質の証明に使えるだけでなく、反例に基づく述語発見においても役に立つ可能性が示唆されている。具体的には、検証の過程でしばしば出現する、「検証上あまり効果がない述語」を見つけて削除することや、プログラムの反例実行パス全体から述語を発見する代わりに、部分的な実行パスから述語を発見することで、述語発見にかかるコストを削減することができるのではないかと考えている。
次に、現状の関数型プログラム検証手法を幅広いプログラムに適用するための大きな課題である、リストや代数的データ型のサポートに取り組んだ。具体的には、それらのデータ型を、オートマトンを用いた抽象化する手法と整数に関する述語を用いた抽象化手法を同時に扱える抽象化手法及び述語発見手法の開発に取り組んだ。抽象化手法についてはいくつかの手法を立案、検討しており、今後、それらの手法を定式化、実装して評価していく予定である。

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

当初の研究では到達可能性解析アルゴリズムを一般のモデル検査アルゴリズムに拡張することとなっていたが、３年目に行う予定であった幅広いデータ型のサポートを優先させることにした。これは、到達可能性という比較的簡単な問題で、幅広いデータ型をサポートすることで、評価に用いるベンチマークプログラムを拡充させ、十分実用的な検証手法を確立してから、検証できる仕様を拡張した方が見通しが良いと判断したからである。
本年度は研究成果を発表こそできていないが、述語抽象化とモデル検査を融合させたアルゴリズムに関する研究成果については著名な国際会議ESOPに投稿し、不採択となったものの、査読者からも研究の技術的な側面については一定の評価を得ており、今後論文のプレゼンテーションを改善して別の国際会議に投稿する予定である。

Strategy for Future Research Activity

まずは、幅広いデータ型をサポートする抽象化手法を確立させ、その手法を実装した関数型プログラム検証器を実装し、様々なプログラムの検証実験を行うことで、手法の性能評価と改善を行う。その後、例外や参照といった副作用をある程度扱えるようにしたり、複雑な仕様を検証できるようにするといった、プログラム検証器の拡張を行い、実用的な関数型プログラム検証器に近づける予定である。