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

使用直接模型检查的功能程序验证方法

• 批准号: 16J01038
• 负责人: 寺尾 拓
• 金额: $ 1.22万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2016
• 资助国家: 日本
• 起止时间: 2016-04-22 至 2019-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-16J01038/
• 关键词: プログラム検証; 関数型プログラム; モデル検査; 高階モデル検査; 述語抽象化; 抽象解釈; 交差型システム

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

In the past year, the research results of "Abstraction of Terms, Formalization and Justification of Fusion of Terms and Conditions" were submitted to the International Society PPDP2019, and oral presentation was conducted. Next, we started with "the development of abstract methods and expression methods for algebraic data types." The purpose of this study is to establish an automatic identification method for the generation of data. The existence of the method of proof is related to the algebra of the type of the property of the "solution""specific elements of the inclusion of the property of the performance of the problem. In this paper, we propose a method of abstracting and describing the algebraic data types at the same time The expression is used in the integer form. The expression is used in the algebraic form. In this paper, we study the expression of algebraic type,"type related expression" and "integer type related expression". We also study the expression of algebraic type related expression. This method is composed of two parts: one part is composed of two parts, the other part is composed of three parts, the other part is composed of four parts. The result of the implementation, the initial goal through the "software" and "specific elements" to express the statement automatically to see the success The research results will be published in the future. The author of the doctoral thesis is responsible for the research and development of the doctoral thesis. To determine the research results of the past three years, to formalize the methods of examination, to complete the manuscript, to complete the doctoral thesis, to examine, to determine.

项目成果

Higher-Order Model Checking in Direct Style

直接风格的高阶模型检查

• DOI: 10.1007/978-3-319-47958-3_16
• 发表时间: 2016
• 期刊: Proceedings of APLAS 2014, LNCS
• 作者: Taku Terao;Taskeshi Tsukada;and Naoki Kobayashi
• 通讯作者: and Naoki Kobayashi

Lazy Abstraction for Higher-Order Program Verification

高阶程序验证的惰性抽象

• DOI: 10.1145/3236950.3236969
• 发表时间: 2018
• 期刊: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming
• 作者: Shinsuke Satoi;Yoh Iwasa;Shinsuke Satoi;Shinsuke Satoi;Terao Taku
• 通讯作者: Terao Taku