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

Research Project

Project/Area Number	24K14898
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60050:Software-related
Research Institution	Kyushu Institute of Technology
Principal Investigator	江本健斗九州工業大学, 大学院情報工学研究院, 准教授 (00587470)
Project Period (FY)	2024-04-01 – 2028-03-31
Project Status	Granted (Fiscal Year 2024)
Budget Amount *help	¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000) Fiscal Year 2027: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000) Fiscal Year 2026: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000) Fiscal Year 2025: ¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000) Fiscal Year 2024: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Keywords	並列プログラミング / プログラミング言語 / 定理証明支援系
Outline of Research at the Start	本研究は、定理証明支援系等による形式的証明（計算機による見落としのない数学的証明）に基づき、正しさや効率に形式的な保証を行える並列プログラミング環境の構築を目標とする。そのために、本研究は以下３つの観点での研究を進める：（１）高レベルな表層プログラミング言語と、それを並列スケルトン（並列プログラムの構成要素）で記述される中間言語へコンパイル（プログラムの変換・効率化）する手法の開発。（２）その中間言語へのコンパイルの正しさやプログラムの効率の変化に対する、定理証明支援系を用いた形式的証明の構築。（３）定理証明支援系での証明を平易に行いやすくするための手法の開発。