Depeeping Sotfware Verifaction Based on Transducer Theory

• Project/Area Number: 24K14891
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: 南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
• Project Period (FY): 2024-04-01 – 2028-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000); Fiscal Year 2027: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000); Fiscal Year 2026: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2025: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2024: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
• Keywords: ソフトウェア検証 / トランスデューサ / 正規表現 / 文字列制約

Outline of Research at the Start

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