プログラム最適化の理論保証に向けた重みつきオートマトン理論の展開

Research Project

Project/Area Number	25K21154
Research Category	Grant-in-Aid for Early-Career Scientists
Allocation Type	Multi-year Fund
Review Section	Basic Section 60010:Theory of informatics-related
Research Institution	Ochanomizu University
Principal Investigator	室屋晃子お茶の水女子大学, 基幹研究院, 講師 (00827454)
Project Period (FY)	2025-04-01 – 2030-03-31
Project Status	Granted (Fiscal Year 2025)
Budget Amount *help	¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000) Fiscal Year 2029: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000) Fiscal Year 2028: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000) Fiscal Year 2027: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000) Fiscal Year 2026: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000) Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Keywords	プログラム最適化 / オートマトン
Outline of Research at the Start	ソフトウェアの高速化を目的とし現代のソフトウェア開発に欠かせないプログラム最適化には、等価性と効率化という2つの要件があり、それらを理論保証することは高信頼ソフトウェアの開発に不可欠である。本研究ではエフェクト付きプログラム一般を対象とし、プログラム実行の抽象度の高い数理モデルと等価性・効率化の正確な定義を提案することで、プログラム最適化の理論保証のための基盤整備を行うことを目的とする。具体的には、ダブル重みつきオートマトンという新奇なオートマトンを導入し、これがエフェクト付きプログラムに対する適切な数理モデルであることをケーススタディおよび一般論の構築により立証する。