| Project/Area Number |
20H05703
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (S)
|
| Allocation Type | Single-year Grants |
|---|
| Review Section |
Broad Section J
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
吉仲 亮 東北大学, 情報科学研究科, 准教授 (80466424)
海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
佐藤 一誠 東京大学, 大学院情報理工学系研究科, 教授 (90610155)
佐藤 亮介 東京農工大学, 学内共同利用施設等, 准教授 (10804677)
|
|---|
| Project Period (FY) |
2020-08-31 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥190,320,000 (Direct Cost: ¥146,400,000、Indirect Cost: ¥43,920,000)
Fiscal Year 2024: ¥39,260,000 (Direct Cost: ¥30,200,000、Indirect Cost: ¥9,060,000)
Fiscal Year 2023: ¥39,260,000 (Direct Cost: ¥30,200,000、Indirect Cost: ¥9,060,000)
Fiscal Year 2022: ¥39,260,000 (Direct Cost: ¥30,200,000、Indirect Cost: ¥9,060,000)
Fiscal Year 2021: ¥39,780,000 (Direct Cost: ¥30,600,000、Indirect Cost: ¥9,180,000)
Fiscal Year 2020: ¥32,760,000 (Direct Cost: ¥25,200,000、Indirect Cost: ¥7,560,000)
|
|---|
| Keywords | プログラム検証 / 高階モデル検査 / 高階不動点論理 / 機械学習 |
|---|
| Outline of Research at the Start |
プログラム検証とは、プログラムが正しく振る舞うかどうかを実行前に網羅的に検証する技術であり、ソフトウェアの信頼性向上のために欠かせないものである。本研究課題では、近年の機械学習技術の台頭とそれに伴うコンピュータによって制御されたシステムの社会への普及を踏まえ、（１）代表者らがこれまで研究を進めてきた高階モデル検査などの自動プログラム検証技術や理論をさらに発展させるとともに、（２）プログラム検証技術のさらなる飛躍のために機械学習技術を活用し、さらに（３）機械学習技術の台頭に伴うソフトウェアの質と量の変化に対応するための、新たなプログラム検証技術の確立を目指す。
|
| Outline of Annual Research Achievements |
研究課題全体を(A)高階モデル検査をはじめとするプログラム検証理論・技術のさらなる発展、(B)プログラム検証への機械学習技術の応用、(C)質の変化したプログラムの検証手法、の3つの課題に分けて並行して研究を進めた。2021年度の主な研究実績（一部、繰越分として2022年度に実施した成果を含む）は以下のとおり。
(A)プログラム検証技術の発展：高階モデル検査の一種である高階不動点論理HFL(Z)の真偽値判定の高速化のため、一階のケースにおいて有効な手法であるPDRと循環証明との間の理論的関係を明らかにした。さらに、リスト構造を扱うプログラムの検証のために、記号オートマトン的関係という概念を新たに導入し、それに基づいてリストに関する性質の自動推論手法の改良を行った。また、並行プログラムの検証手法として、π計算と呼ばれる並行計算モデルで記述された並行プログラムの停止性を逐次プログラムの停止性に帰着する手法を考案し、実装・評価を行った。
(B)プログラム検証への機械学習技術の応用：プログラム検証において鍵となるループ不変条件等の発見のためにニューラルネットワークを用いる枠組み（NeuGus: Neural Network-Guided Synthesis）を考案・実装し、不動点論理ソルバの一種であるCHCソルバHoIceに組み込んでその有効性を確認した。
(C)質の変化したプログラムの検証手法： ニューラルネットワークを組み込んだソフトウェアの検証に向け、(B)のNeuGuSの枠組みを利用して、ニューラルネットワークから通常のプログラムコンポーネントを合成する手法を考案し、その有効性を確認した。また、確率付きプログラムの検証のための基礎として、確率付き高階不動点論理について研究を行い、モデル検査が決定可能なクラスを明らかにした。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要に述べた通り順調に研究成果が出ており、一流の雑誌や国際会議に論文を発表している。
|
| Strategy for Future Research Activity |
海外からの研究員の着任が遅れたことによって一部先延ばししていた機械学習のプログラム検証への応用部分の研究をさらに進める。
|
| Assessment Rating |
Interim Assessment Comments (Rating)
A: In light of the aim of introducing the research area into the research categories, the expected progress has been made in research.
|
