hyperpropertyと余代数的時相論理の融合とそのプログラム検証への応用

• Project/Area Number: 25K21183
• Research Category: Grant-in-Aid for Early-Career Scientists
• Allocation Type: Multi-year Fund
• Review Section: Basic Section 60050:Software-related
• Research Institution: Waseda University
• Principal Investigator: 内藏 理史 早稲田大学, 教育・総合科学学術院, 講師(任期付) (10969364)
• Project Period (FY): 2025-04-01 – 2030-03-31
• Project Status: Granted (Fiscal Year 2025)
• Budget Amount: ¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,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: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2025: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
• Keywords: 形式検証 / モデル検査 / hyperproperty / 圏論

Outline of Research at the Start

形式検証はソフトウェアの信頼性を高めるために研究されている．検証の対象となる性質は多岐にわたる．その中でも，不干渉性や差分プライバシーのような関係的性質を含む，hyperpropertyと呼ばれるクラスの性質を対象とする研究が近年注目されており，時相論理の拡張を通した自動検証の研究が行われている．本研究ではhyperpropertyのための時相論理に対してより数学的・理論的にアプローチすることで形式検証技術の更なる発展を目指す．具体的な方向としては圏論を用いた余代数的時相論理の枠組みとhyperpropertyを融合することで，背後にある数学的構造をうまく捉えた新しい検証手法の獲得を目指す．