トランスデューサ理論に基づくソフトウェア検証の深化

• 研究課題/領域番号: 24K14891
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60050:ソフトウェア関連
• 研究機関: 東京工業大学
• 研究代表者: 南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
• 研究期間 (年度): 2024-04-01 – 2028-03-31
• 研究課題ステータス: 交付 (2024年度)
• 配分額: 4,030千円 (直接経費: 3,100千円、間接経費: 930千円); 2027年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2026年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2025年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2024年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
• キーワード: ソフトウェア検証 / トランスデューサ / 正規表現 / 文字列制約

研究開始時の研究の概要

トランスデューサ理論に基づくソフトウェア検証技術について，木トランスデューサの理論に基づく正規表現マッチングの計算量解析およびストリーミングトランスデューサとParikhオートマトンの理論に基づく文字列制約の充足可能性判定を中心に研究を行う．また，トランスデューサ理論を証明支援系により形式化し，信頼性の高い検証技術を構築する基盤を整備する．