| 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
|
| 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で記述されたシステムプログラムに対する自動検証ツールを実現する。
|
