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

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

基本信息

批准号：
12J08057
负责人：
佐藤亮介
金额：
$ 1.28万
依托单位：
The University of Tokyo (2013)Tohoku University (2012)
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2012
资助国家：
日本
起止时间：
2012 至 2013
项目状态：
已结题

项目摘要

高階モデル検査を用いた高階関数型言語のためのソフトウェアモデル検査器の拡張に関する研究を進め、その成果を論文として投稿した。検証の枠組みの拡張として、既存の高階関数型言語のための自動検証手法では扱えなかった関数の等価性や単調性などの関数の性質を扱えるようにした。具体的には、このような関数の性質に関する検証問題を既存の検証手法で扱える問題に帰着する方法を提案した。既存の高階関数型プログラムの自動検証手法のほとんどは、量化子を含まない一階の述語を用いてプログラムを抽象化することによって検証を行っている。しかし、量化子を含まない一階の述語という制限のため、関数の等価性など、全称や関数を用いないと表すことができない性質を扱えなかった。例えば、次のように定義された二つの関数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のサブセットで書かれたプログラムを対象とする検証器のプロトタイプを実装した。実装した検証器をさまざまなプログラムに適用し、本手法の有効性を確かめた。ここまでに得られた成果を国内会議の場で発表し、同時に他の研究者との意見交換を行った。

我们已经对使用高阶模型检查的高阶功能语言扩展软件模型检查器进行了研究，并将结果作为论文提交。作为验证框架的扩展，我们使能够处理诸如等效性和单调性之类的功能，这些功能无法通过现有的自动验证方法来处理高阶功能语言。具体而言，我们提出了一种将有关此类功能属性的验证问题减少到可以通过现有验证方法来处理的问题。通过使用不包含量化器的一阶谓词将程序抽象来验证大多数现有的用于高阶功能程序的自动验证方法。但是，由于不包含量化器的一阶谓词的限制，因此不可能处理不使用全名或函数（例如函数等效度）无法表达的属性。例如，不可能验证两个函数总和定义为如下的sum2是相等的。令rec sum n =如果n <0，则0否n + sum（n-l）令rec umac n m =如果n <0，则m el se umac（n-1）（n + m）令sum2 n = umacc n 0其中，总和是一个求出一个函数的函数，该函数从1到n，而sum2则使用累积可变来计算sum2。在这项研究中，我们提出了一种方法，以减少不使用一般名称和功能的验证问题来减少属性的验证问题，而仅处理现有一阶谓词的验证问题。基于此扩展验证框架，我们实现了用功能语言OCAML子集编写的验证者定位程序的原型。实施的验证者已应用于各种程序，以验证该方法的有效性。到目前为止获得的结果是在国内会议上提出的，与此同时，他们与其他研究人员交换了意见。

项目成果

期刊论文数量（0）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

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)
影响因子：
0
作者：
Ryosuke Sato;Hiroshi Unno;Naoki Kobayashi
通讯作者：
Naoki Kobayashi

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

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