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

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

• 批准号: 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のプロトタイプを実装した。実験の結果、当初の目標通り「ソートされたリスト」や「特定の要素を含むリスト」を表現する述語を自動で発見することに成功した。この研究成果について今後論文にまとめ、国際学会に投稿する予定である。また、これらの成果を合わせて博士論文の執筆を行った。想定より３年間の研究成果をまとめた検証手法の定式化に時間がかかり、期日までに原稿が完成に至らなかったため、今後、なるべく早急に博士論文を完成させ、審査を受ける予定である。

首先，从上一年的研究中获得了“融合谓词抽象和模型检查的算法的理由和理由”的结果，并将其提交给国际科学学会PPDP 2019，并进行了口头介绍。接下来，我们开始“开发支持代数数据类型的抽象和谓词发现方法”。这项研究的目的是建立所需的自动验证方法，以支持列表和代数数据类型。现有的验证方法的问题是，无法正确表达与代数数据类型（例如“排序列表””和“包含特定元素的列表”相关的属性。在这项研究中，为了同时处理整数和代数数据类型，我们提出了一种方法，其中代表代数数据类型的自动机状态通过“数据满足数据满足的局部谓词”的区分，并开发了一种使用抽象方法和号角约束问题的代数数据的谓词发现方法。这种谓词发现技术通常用作整数类型的谓词发现，但尚未用于代数数据类型。因此，在这项研究中，我们决定将代数数据类型的谓词发现分为“与数据形状有关的谓词”和“数据中嵌入数据中的整数类型的谓词”，并使用不同的算法发现谓词。这些技术被合并以实现支持代数数据类型的DMOCHI程序化自动验证系统的原型。由于实验，我们成功地自动发现了代表“排序列表”和“包含特定元素”的谓词，最初是针对的。这项研究的结果将在将来汇编成一篇论文，并提交给国际科学学会。他还将这些结果结合在一起，写了他的博士学位论文。制定了一种验证方法的时间比预期的要长，该方法总结了过去三年的研究结果，并且截止日期未完成手稿，因此我们计划尽快完成博士学位论文并接受考试。

项目成果

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