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

点击翻译按钮获取中文摘要

まず、前年度の研究で得られた「述語抽象化とモデル検査の融合アルゴリズムの定式化及び正当性証明」に関する成果を論文にまとめ、国際学会PPDP2019に投稿し、採択され、口頭発表を行った。次に、「代数的データ型をサポートする抽象化手法および述語発見手法の開発」に着手した。この研究の目的は、リストや代数的データ型をサポートする必要した自動検証手法の確立である。既存の検証手法では代数的データ型に関する性質のうち「ソートされたリスト」や「特定の要素を含むリスト」のような性質をうまく表現できないという問題があった。本研究では、整数型と代数的データ型を同時に扱うために、代数的データ型を表すオートマトンの状態を「そのデータが満たす局所的な述語」によって区別するという手法を提案し、抽象化手法およびHorn節制約問題を用いた代数的データ型に対する述語発見手法を開発した。この述語発見手法は整数型に対する述語発見としてよく用いられているが、代数的データ型には用いられていなかった。そこで本研究では、代数的データ型の述語発見を、「データの形に関する述語」と「データに埋め込まれた整数型の述語」に分けて、それぞれを異なるアルゴリズムによって述語発見することにした。これらの手法を組み合わせて、代数的データ型をサポートするプログラム自動検証システムDMoCHiのプロトタイプを実装した。実験の結果、当初の目標通り「ソートされたリスト」や「特定の要素を含むリスト」を表現する述語を自動で発見することに成功した。この研究成果について今後論文にまとめ、国際学会に投稿する予定である。また、これらの成果を合わせて博士論文の執筆を行った。想定より３年間の研究成果をまとめた検証手法の定式化に時間がかかり、期日までに原稿が完成に至らなかったため、今後、なるべく早急に博士論文を完成させ、審査を受ける予定である。