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

• 研究課題/領域番号: 25H00446
• 研究種目: 基盤研究(S)
• 配分区分: 補助金
• 審査区分: 大区分J
• 研究機関: 東北大学
• 研究代表者: 海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
• 研究分担者: 塚田 武志 千葉大学, 大学院理学研究院, 教授 (50758951) ; 内藏 理史 早稲田大学, 教育・総合科学学術院, 講師(任期付) (10969364) ; 川島 英之 慶應義塾大学, 環境情報学部(藤沢), 准教授 (90407148) ; 龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
• 研究期間 (年度): 2025-04-01 – 2030-03-31
• 研究課題ステータス: 交付 (2025年度)
• 配分額: 201,630千円 (直接経費: 155,100千円、間接経費: 46,530千円); 2025年度: 33,410千円 (直接経費: 25,700千円、間接経費: 7,710千円)
• キーワード: プログラム検証 / 論理学 / 計算論 / 最適化理論 / 学習理論

研究開始時の研究の概要

現代社会においては、重要な社会基盤がコンピュータにより制御されており、それを動かすソフトウェアが意図通りに動作することを数学的に保証する「プログラム検証技術」の重要性が高まっている。しかし、最先端の検証技術は場当たり的な改善の繰り返しによって複雑化し、論理的誤りや拡張性の欠如が見られる。本研究では、このような状況を打破するために、計算論・論理学に加え学習理論・最適化理論を用い、ヒューリスティックスにも踏み込んだ検証技術の基礎付けを行う。さらに、応用分野の要請に応じて拡張し、並行・並列・分散システム、暗号・確率システム、CやRustで記述されたシステムプログラムに対する自動検証ツールを実現する。