• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Foundations and Applications of Program Verification Techniques

Research Project

Project/Area Number 25H00446
Research Category

Grant-in-Aid for Scientific Research (S)

Allocation TypeSingle-year Grants
Review Section Broad Section J
Research InstitutionTohoku University

Principal Investigator

海野 広志  東北大学, 電気通信研究所, 教授 (80569575)

Co-Investigator(Kenkyū-buntansha) 塚田 武志  千葉大学, 大学院理学研究院, 教授 (50758951)
内藏 理史  早稲田大学, 教育・総合科学学術院, 講師(任期付) (10969364)
川島 英之  慶應義塾大学, 環境情報学部(藤沢), 准教授 (90407148)
龍田 真  国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
Project Period (FY) 2025-04-01 – 2030-03-31
Project Status Granted (Fiscal Year 2025)
Budget Amount *help
¥201,630,000 (Direct Cost: ¥155,100,000、Indirect Cost: ¥46,530,000)
Fiscal Year 2025: ¥33,410,000 (Direct Cost: ¥25,700,000、Indirect Cost: ¥7,710,000)
Keywordsプログラム検証 / 論理学 / 計算論 / 最適化理論 / 学習理論
Outline of Research at the Start

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

Report

(2 results)
  • 2025 Abstract ( PDF )   Comments on the Screening Results

URL: 

Published: 2025-04-17   Modified: 2025-06-20  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi