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

• 研究課題/領域番号: 25K21154
• 研究種目: 若手研究
• 配分区分: 基金
• 審査区分: 小区分60010:情報学基礎論関連
• 研究機関: お茶の水女子大学
• 研究代表者: 室屋 晃子 お茶の水女子大学, 基幹研究院, 講師 (00827454)
• 研究期間 (年度): 2025-04-01 – 2030-03-31
• 研究課題ステータス: 交付 (2025年度)
• 配分額: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円); 2029年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2028年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2027年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2026年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2025年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
• キーワード: プログラム最適化 / オートマトン

研究開始時の研究の概要

ソフトウェアの高速化を目的とし現代のソフトウェア開発に欠かせないプログラム最適化には、等価性と効率化という2つの要件があり、それらを理論保証することは高信頼ソフトウェアの開発に不可欠である。
本研究ではエフェクト付きプログラム一般を対象とし、プログラム実行の抽象度の高い数理モデルと等価性・効率化の正確な定義を提案することで、プログラム最適化の理論保証のための基盤整備を行うことを目的とする。
具体的には、ダブル重みつきオートマトンという新奇なオートマトンを導入し、これがエフェクト付きプログラムに対する適切な数理モデルであることをケーススタディおよび一般論の構築により立証する。