正しさと効率の保証を備えた平易な並列プログラミング環境の構築に関する研究

• 研究課題/領域番号: 24K14898
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60050:ソフトウェア関連
• 研究機関: 九州工業大学
• 研究代表者: 江本 健斗 九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
• 研究期間 (年度): 2024-04-01 – 2028-03-31
• 研究課題ステータス: 交付 (2024年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2027年度: 390千円 (直接経費: 300千円、間接経費: 90千円); 2026年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2025年度: 2,860千円 (直接経費: 2,200千円、間接経費: 660千円); 2024年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
• キーワード: 並列プログラミング / プログラミング言語 / 定理証明支援系

研究開始時の研究の概要

本研究は、定理証明支援系等による形式的証明（計算機による見落としのない数学的証明）に基づき、正しさや効率に形式的な保証を行える並列プログラミング環境の構築を目標とする。
そのために、本研究は以下３つの観点での研究を進める：
（１）高レベルな表層プログラミング言語と、それを並列スケルトン（並列プログラムの構成要素）で記述される中間言語へコンパイル（プログラムの変換・効率化）する手法の開発。
（２）その中間言語へのコンパイルの正しさやプログラムの効率の変化に対する、定理証明支援系を用いた形式的証明の構築。
（３）定理証明支援系での証明を平易に行いやすくするための手法の開発。