| 研究課題/領域番号 |
17H01720
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 早稲田大学 |
|---|
研究代表者 |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| 研究分担者 |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2022-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
17,940千円 (直接経費: 13,800千円、間接経費: 4,140千円)
2021年度: 3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2020年度: 3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2019年度: 3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2018年度: 3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2017年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
|
|---|
| キーワード | プログラム検証 / 不動点論理 / 型システム / 自動定理証明 / 分離論理 / 循環証明 / 代数的エフェクト / ソフトウェアモデル検査 / プログラミング言語 / プログラム論理 |
|---|
| 研究成果の概要 |
以下の研究成果を得た。(1)高階プログラムの時相的仕様についての研究成果。(2)再帰的(帰納的・余帰納的)な述語定義を書くことのできる一階不動点論理や関連する数学的帰納法の形式化である循環証明体系についての研究成果。(3)破壊的代入など様々な計算効果を統一的に扱える先進的言語機能である代数的エフェクトハンドラについての研究成果。(4)サイドチャネルやReDoS攻撃の検出・防衛などプログラム検証・合成技術のセキュリティへの応用に関する研究成果。(5)後方参照、先読みといった拡張機能を含む拡張正規表現の形式言語理論についての研究成果。
|
| 研究成果の学術的意義や社会的意義 |
非決定的動作を含む高階プログラムについて初の相対的完全な検証を実現するリファインメント型システムの提案、様々な問題の解決に応用できる一階不動点論理の妥当性判定のための新しいアルゴリズムを提案、深刻なセキュリティ脅威であるReDoS脆弱性を修復するため初のプログラム合成手法の提案など、本研究はこれまでのプログラミング言語・形式検証・定理証明・セキュリティの研究を大きく飛躍させた。よって、本研究の成果は極めて高い学術的および社会的意義を持つと考える。
|
