高階再帰スキームのモデル検査とそのプログラム検証への応用

高阶递归方案的模型检验及其在程序验证中的应用

基本信息

批准号：
10J03842
负责人：
塚田武志
金额：
$ 1.34万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2010
资助国家：
日本
起止时间：
2010 至 2012
项目状态：
已结题

项目摘要

前年度に引き続いた理論的な側面の研究と、そのプログラム検証への応用について研究を行った。1.ゲーム意味論と共通型理論の融合ゲーム意味論と共通型理論は、高階再帰スキームモデル検査問題への2つの主要なアプローチである。この2つのアプローチの関係を明らかにすることは未解決の課題であったが、我々は2つの結びつける理論(2レベルゲーム意味論)を構築することに成功した。また、この理論を応用することで既知のモデル検査アルゴリズムの計算量の新しい上界など、応用上有用な結果を与えた。2.ゲーム意味論に基づいた新しい高階再帰スキームモデル検査器ゲーム意味論に基づいた新しい高階再帰スキームモデル検査器を提案し、その評価を行った。まず、上で与えたゲーム意味論と共通型理論の対応関係を利用して、ゲーム意味論に基づく共通型の推論法を与えた。この推論法は一般には停止するとは限らないものであるが、この手法と抽象実行という技術を組み合わせることで必ず停止するアルゴリズムを得ることができる。高階再帰スキームのモデル検査は共通型の検査・推論に帰着できることが知られているため、得られた共通型推論器はモデル検査器として使うことができる。こうして得られたアルゴリズムが、特定の場合には既存の手法よりも優れていることを、実験的に確かめた。高階再帰スキームモデル検査はプログラム検証の際のボトルネックであり、この高速化はプログラム検証器の実用化にとって大変重要である。

我们对上一年持续的理论方面及其在计划验证中的应用进行了研究。 1。游戏语义和常见类型理论游戏语义和共同类型理论的融合是高阶递归方案模型检查问题的两种主要方法。尽管未解决的问题尚未解决以阐明这两种方法之间的关系，但我们成功地构建了两个链接理论（两级游戏语义）。此外，应用该理论提供了有用的结果，例如已知模型检查算法的计算复杂性中的新上限。 2。基于游戏语义基于游戏语义的新的高阶递归方案模型检查器，提出了基于游戏语义的新的高阶递归方案模型检查器。首先，我们使用了上面给出的游戏语义和公共类型理论之间的对应关系，以基于游戏语义的方式提供一种公共类型的推理方法。这种推论方法通常不会停止，而是通过将此技术与抽象执行技术相结合，即可以获得总是停止的算法。由于知道对高阶递归方案的模型检查可以从公共类型检查和推断中得出，因此获得的常见类型推断可以用作模型检查设备。经过实验证实，在某些情况下，因此获得的算法优于现有方法。验证程序时，高阶递归方案模型检查是一种瓶颈，对于实际应用程序验证者非常重要。