| 研究課題/領域番号 |
15K15974
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 九州工業大学 |
|---|
研究代表者 |
江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| 研究課題ステータス |
完了 (2018年度)
|
| 配分額 *注記 |
4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2018年度: 390千円 (直接経費: 300千円、間接経費: 90千円)
2017年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2016年度: 2,730千円 (直接経費: 2,100千円、間接経費: 630千円)
2015年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 定理証明支援系 / 並列プログラミング / 計算量 / 不等式 / 並列 / 並列スケルトン / グラフ / 機械証明 |
|---|
| 研究成果の概要 |
本研究では、正しさのみでなく、その並列計算量（実行時間）をも形式的に保証できるような並列プログラミング環境の構築を目指し、そのための基盤技術として、大きく次の二点についての成果を得た：（１）局所計算量をプログラム中に自然に併記できるモナドに基づく逐次計算量の形式的記述手法の並列計算量への拡張、（２）定理証明支援系における不等式などの扱いを簡潔にし、計算量証明を行いやすくする技術。これらにより、並列実行の仕組みに制限はあるものの、機械により速さと正しさが保証される並列プログラムの開発が容易になった。
|
| 研究成果の学術的意義や社会的意義 |
身の回りにあふれるコンピュータが安全かつ効率的に仕事をしているのは、その仕事の指示をしているプログラムが「正しく・速く」動くように作られているからである。しかし、どのような専門家であっても、人である以上、見落としなく「正しさ」と「速さ」を保証したプログラムを作ることはできない。そのため、人ではなく、見落としをしないコンピューター自身にその「正しさ」と「速さ」を保証させることが理想である。残念なことに、コンピュータにその保証をさせるにも煩雑な手順が必要であり、コストが掛かってしまう。本研究は、その手順を簡単化する手法を開発し、そのコストを下げることでより安全かつ効率的な社会の実現に貢献する。
|
