| 研究課題/領域番号 |
16H05856
|
|---|
| 研究種目 |
若手研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2020-03-31
|
| 研究課題ステータス |
完了 (2019年度)
|
| 配分額 *注記 |
14,560千円 (直接経費: 11,200千円、間接経費: 3,360千円)
2019年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2018年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2017年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2016年度: 4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
|
|---|
| キーワード | プログラム検証 / プログラミング言語 / 関係的仕様 / 時相的仕様 / 依存リファインメント型 / ホーン節制約解消 / 不動点論理 / 帰納的定理証明 / 時相的・関係的仕様 / 述語制約解消 / 不変条件 / ランキング関数 / スコーレム関数 / リファインメント型 / 不動点制約解消 / 述語充足可能性判定 / 循環証明 / 依存型 / プログラム合成 / 動的論理 / 再帰データ型 |
|---|
| 研究成果の概要 |
本研究では、ソフトウェアの信頼性向上を目的とし、これまで研究代表者らが提案してきたリファインメント型システムやホーン節制約解消法といった高レベル言語のための検証理論とそれに基づく全自動検証ツールRCamlを発展させ、高レベルプログラムの関係的・時相的仕様検証を実現した。特に、関係的仕様検証が可能な（余）帰納的定理証明に基づくホーン節制約解消法および時相的仕様検証が可能な不動点論理制約解消法を世界で初めて実現した。
|
| 研究成果の学術的意義や社会的意義 |
本研究で提案した高レベルプログラムの時相的・関係的検証のためのリファインメント型システム、不動点論理、動的論理といった検証理論・手法は、既存手法が扱えなかった高階関数や代数データ型といった発展的な言語機能を扱うことを可能とした。また、本研究では、提案した検証理論に基づき、高階関数型言語 OCaml のための検証ツール RCaml、不動点論理制約解消ツール MuVal、述語制約解消ツール PCSat の開発も行っており、今後これらのツールを実際のソフトウェア開発現場で実用可能なレベルまで発展させれば、ソフトウェアの信頼性向上に大きく貢献することが期待される。
|
