权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Program Verification Based on Higher-Order Fixpoint Logic

基于高阶不动点逻辑的程序验证

基本信息

批准号：
20H00577
负责人：
小林直樹
金额：
$ 28.45万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (A)
财政年份：
2020
资助国家：
日本
起止时间：
2020-04-01 至 2021-03-31
项目状态：
已结题

项目摘要

様々な重要な社会基盤がコンピュータによって制御されている今日，ソフトウェアが期待通りの動作をすることを保証するためのプログラム検証技術は今後ますます重要になる．我々はシステム検証技術の主流であるモデル検査の真の拡張である高階モデル検査とそれに基づくプログラム検証手法について世界をリードしてきたが，最近になって高階モデル検査の中でも高階不動点論理に基づく方式が特に有望であることを見出した．そこで本研究では高階不動点論理に基づくプログラム検証の理論をさらに発展させるとともに，他の関連する理論・技術と組み合わせることによって，高階モデル検査に基づくプログラム自動検証手法を実用レベルにまで昇華させることを目指した．採択後数か月で廃止になったため、上記目的の達成には至っていないが、これまでに以下の研究を行った。まず、最大不動点のみを持つ高階不動点論理に整数を加えて拡張したνHFL(Z)の論理式の真偽値判定手法として、(1) 述語抽象化と高階モデル検査を組み合わせる方式、(2)詳細型システムにおける型推論問題に帰着する方式、の2種類について並行して研究を進め、両者に基づくνHFL(Z)の論理式の自動真偽値判定ツールPaHFLおよびRetHFLを構築した。さらにそれらのツールをプログラムの自動検証に応用し、既存の同目的のツールHorusよりも優れた性能を示すことを確認した。また、前年度から取り組んでいた高階不動点論理に確率を加えて拡張した確率付き高階不動点論理PHFLの研究を継続し、PHFLモデル検査問題の困難性を解析階層（analytical hierarchy)を用いて特徴づけるとともに、型システムを用いて決定可能な部分クラスを与えた。

The important social foundation is to ensure that the future of science and technology will be more important. We are currently in the mainstream of science and technology, and we are looking forward to seeing the higher-order fixed point logic in the higher-order fixed point logic. In this study, higher-order fixed point logic is used to develop theories and techniques for automatic detection of higher-order fixed points. After the acquisition, the number of months to stop, the goal to achieve, the following research (1) A method for determining the truth of a logical expression of HFL(Z) by adding integers to the maximum fixed point,(2) A method for determining the truth of a logical expression of HFL(Z) by adding integers to the maximum fixed point, and (3) A method for determining the truth of a logical expression of HFL(Z) by adding integers to the maximum fixed point,(4) A method for determining the truth of a logical expression of HFL (Z) by adding integers to the maximum fixed point, and (5) A method for determining the truth of a logical expression of HFL (Z) by adding integers to the maximum fixed point. Automatic True/False Value Determination of the Logic Expression of the Base HFL(Z) For example, if you want to check the status of the server, you can check the status of the server. In the previous year, the accuracy rate of high-order fixed point logic was increased, and the accuracy rate was increased. The research on high-order fixed point logic PHFL was carried out. The difficulty of checking the problem was analyzed in the analytical hierarchy. The characteristics of the problem were determined.