高階関数型言語のためのソフトウェアモデル検査

高阶函数语言的软件模型检查

• 批准号: 12J08057
• 负责人: 佐藤 亮介
• 金额: $ 1.28万
• 依托单位: The University of Tokyo (2013)Tohoku University (2012)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2012
• 资助国家: 日本
• 起止时间: 2012 至 2013
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-12J08057/
• 关键词: 高階関数型言語; 高階モデル検査; ソフトウェアモデル検査; 詳細化型; 継続渡し形式変換; 述語抽象化

高階モデル検査を用いた高階関数型言語のためのソフトウェアモデル検査器の拡張に関する研究を進め、その成果を論文として投稿した。検証の枠組みの拡張として、既存の高階関数型言語のための自動検証手法では扱えなかった関数の等価性や単調性などの関数の性質を扱えるようにした。具体的には、このような関数の性質に関する検証問題を既存の検証手法で扱える問題に帰着する方法を提案した。既存の高階関数型プログラムの自動検証手法のほとんどは、量化子を含まない一階の述語を用いてプログラムを抽象化することによって検証を行っている。しかし、量化子を含まない一階の述語という制限のため、関数の等価性など、全称や関数を用いないと表すことができない性質を扱えなかった。例えば、次のように定義された二つの関数sum、sum2が等しいということが検証できない。let rec sum n = if n <0 then 0 else n + sum (n-l)let rec sumacc n m = if n <0 then m el se sumacc (n-1) (n+m)let sum2 n = sumacc n 0ここで、sumは1からnまでの整数の和を求める関数であり、sum2はそれを累積変数を用いて求めるものである。本研究では、このような全称および関数を用いないと表せない性質の検証問題を、既存の一階の述語のみを扱う検証問題に帰着する方法を提案した。この拡張した検証の枠祖みを基に、関数型言語OCamlのサブセットで書かれたプログラムを対象とする検証器のプロトタイプを実装した。実装した検証器をさまざまなプログラムに適用し、本手法の有効性を確かめた。ここまでに得られた成果を国内会議の場で発表し、同時に他の研究者との意見交換を行った。

The research on the application of high-level digital language in high-level digital language detection has been carried out and the results have been submitted The test results show that there is a high correlation between the number of words and the number of words. Specific questions, questions, questions. The automatic detection method of existing high-order correlation type is used to abstract the first order expression, and the quantizer is used to detect the first order expression. The first order of quantifiers is limited to the first order of quantifiers. The second order of quantifiers is limited to the first order of quantifiers. The third order of quantifiers is limited to the first order of quantifiers. The fourth order of quantifiers is limited to the second order of quantifiers. The fourth order of quantifiers is limited to the third order of quantifiers. The fourth order of quantifiers is limited to the fourth order of quantifiers. For example, let rec sum n = if n <0 then 0 else n + sum (n-l)let rec sumacc n m = if n <0 then m el se sumacc (n-1) (n+m)let sum2 n = sumacc n 0, sum 1 n integer This research proposes methods to verify the nature of the full name and relevant numbers, and to verify the meaning of existing first-order terms. This is the first time that a digital language has been used in a digital language. This method is applicable to all kinds of equipment and equipment. The results of this study were presented at domestic conferences and exchanged views with other researchers.

项目成果

Towards a scalable software model checker for higher-order programs

面向高阶程序的可扩展软件模型检查器

• DOI: 10.1145/2426890.2426900
• 发表时间: 2013
• 期刊: Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation (PEPM 2013)
• 作者: Ryosuke Sato;Hiroshi Unno;Naoki Kobayashi
• 通讯作者: Naoki Kobayashi

一階詳細化を用いた関数型プログラムの関係的性質の検証

使用一阶细化验证函数程序的关系属性

• 发表时间: 2014
• 作者: K. Kawaguchi;S. -i. Sasa;and T. Sagawa;吉村雅美;佐藤亮介
• 通讯作者: 佐藤亮介

MoCHi: Software Model Checker for a Higher-Order Functional Language

MoCHi：高阶函数语言的软件模型检查器

• 发表时间: 2012
• 作者: 川口喬吾;中山洋平;吉村 雅美;Ryosuke Sato;Kyogo Kawaguchi and Yohei Nakayama;Ryosuke Sato
• 通讯作者: Ryosuke Sato