| 研究課題/領域番号 |
20H00577
|
|---|
| 研究種目 |
基盤研究(A)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
中区分60:情報科学、情報工学およびその関連分野
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2021-03-31
|
| 研究課題ステータス |
中途終了 (2020年度)
|
| 配分額 *注記 |
44,460千円 (直接経費: 34,200千円、間接経費: 10,260千円)
2020年度: 9,620千円 (直接経費: 7,400千円、間接経費: 2,220千円)
|
|---|
| キーワード | プログラム検証 / 高階不動点論理 / 確率付き高階不動点論理 / モデル検査 / 高階モデル検査 |
|---|
| 研究開始時の研究の概要 |
様々な重要な社会基盤がコンピュータによって制御されている今日，ソフトウェアが期待通りの動作をすることを保証するためのプログラム検証技術は今後ますます重要になる．本研究課題では，プログラム検証問題を「高階不動点論理」とよばれる論理における恒真性判定問題（与えられた論理式が真であるか否かを判定する問題）に帰着することによって，プログラムの全自動検証を可能にする理論・技術について研究を行う．
|
| 研究実績の概要 |
様々な重要な社会基盤がコンピュータによって制御されている今日，ソフトウェアが期待通りの動作をすることを保証するためのプログラム検証技術は今後ますます重要になる．我々はシステム検証技術の主流であるモデル検査の真の拡張である高階モデル検査とそれに基づくプログラム検証手法について世界をリードしてきたが，最近になって高階モデル検査の中でも高階不動点論理に基づく方式が特に有望であることを見出した．そこで本研究では高階不動点論理に基づくプログラム検証の理論をさらに発展させるとともに，他の関連する理論・技術と組み合わせることによって，高階モデル検査に基づくプログラム自動検証手法を実用レベルにまで昇華させることを目指した．採択後数か月で廃止になったため、上記目的の達成には至っていないが、これまでに以下の研究を行った。
まず、最大不動点のみを持つ高階不動点論理に整数を加えて拡張したνHFL(Z)の論理式の真偽値判定手法として、(1) 述語抽象化と高階モデル検査を組み合わせる方式、(2)詳細型システムにおける型推論問題に帰着する方式、の2種類について並行して研究を進め、両者に基づくνHFL(Z)の論理式の自動真偽値判定ツールPaHFLおよびRetHFLを構築した。さらにそれらのツールをプログラムの自動検証に応用し、既存の同目的のツールHorusよりも優れた性能を示すことを確認した。
また、前年度から取り組んでいた高階不動点論理に確率を加えて拡張した確率付き高階不動点論理PHFLの研究を継続し、PHFLモデル検査問題の困難性を解析階層（analytical hierarchy)を用いて特徴づけるとともに、型システムを用いて決定可能な部分クラスを与えた。
|
| 現在までの達成度 (段落) |
令和2年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
令和2年度が最終年度であるため、記入しない。
|
