プログラム検証技術の基礎付けと応用

2025 Fiscal Year Comments on the Screening Results

• Project/Area Number: 25H00446
• Research Category: Grant-in-Aid for Scientific Research (S)
• Allocation Type: Single-year Grants
• Review Section: Broad Section J
• Research Institution: Tohoku University
• Principal Investigator: 海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
• Co-Investigator(Kenkyū-buntansha): 塚田 武志 千葉大学, 大学院理学研究院, 教授 (50758951) ; 内藏 理史 早稲田大学, 教育・総合科学学術院, 講師(任期付) (10969364) ; 川島 英之 慶應義塾大学, 環境情報学部(藤沢), 准教授 (90407148) ; 龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
• Project Period (FY): 2025-04-01 – 2030-03-31

Scientific Significance and Expected Research Achievements

本研究は、プログラム検証技術の実現を目指しているもので、応募者らによって発展してきた述語制約と不動点論理、循環証明と証明洗練による検証技術は独自性、独創性がある。これらの理論的基盤を他の学習理論や最適化理論と融合し、深化させることで多様な検証対象へ拡張するというアイデアは確実性が高い。また、既存の様々な技法に対する統一的理論を構築し、既存の様々な技法のもつ拡張性と正確性を明らかにしようとする挑戦的な取組である。