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

2025 年度 審査結果の所見

• 研究課題/領域番号: 25H00446
• 研究種目: 基盤研究(S)
• 配分区分: 補助金
• 審査区分: 大区分J
• 研究機関: 東北大学
• 研究代表者: 海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
• 研究分担者: 塚田 武志 千葉大学, 大学院理学研究院, 教授 (50758951) ; 内藏 理史 早稲田大学, 教育・総合科学学術院, 講師(任期付) (10969364) ; 川島 英之 慶應義塾大学, 環境情報学部(藤沢), 准教授 (90407148) ; 龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
• 研究期間 (年度): 2025-04-01 – 2030-03-31

学術的意義、期待される成果

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