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

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

• 批准号: 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，被接受，并做了口头报告.接下来，我们开始“开发支持代数数据类型的抽象方法和谓词发现方法。”本研究的目的是建立一种支持列表和代数数据类型的自动验证方法。现有的验证方法存在无法充分表达与代数数据类型相关的属性的问题，例如“排序列表”和“包含特定元素的列表”。在本研究中，为了同时处理整数类型和代数数据类型，我们提出了一种通过“数据满足的局部谓词”来区分表示代数数据类型的自动机状态的方法，并且我们使用抽象方法和我们使用 Horn 子句约束问题开发了代数数据类型的谓词发现方法。这种谓词发现方法通常用于发现整数类型的谓词，但尚未用于代数数据类型。因此，在本研究中，我们将代数数据类型的谓词发现分为“与数据形状相关的谓词”和“嵌入数据中的整数类型的谓词”，并决定使用不同的算法来发现每种谓词。通过结合这些方法，我们实现了 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