Integration of Theorem Prover and Model Checker with Automatic Library Search for Large-Scale Formal Verification

Research Project

Project/Area Number	25K14989
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60010:Theory of informatics-related
Research Institution	Shinshu University
Principal Investigator	和崎克己信州大学, 学術研究院工学系, 教授 (70271492)
Project Period (FY)	2025-04-01 – 2029-03-31
Project Status	Granted (Fiscal Year 2025)
Budget Amount *help	¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000) Fiscal Year 2028: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000) Fiscal Year 2027: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000) Fiscal Year 2026: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000) Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Keywords	定理証明系 / モデル検査 / 大規模言語モデル / ハードウェアコンパイラ / 状態空間最適分割
Outline of Research at the Start	本研究は、定理証明系とモデル検査器を統合し、大規模かつ高並列なハードウェア設計に対する高精度な検証を実現することを目的とする。AIによる定理検索機能を備えたコンパイラとGPUクラスタによる並列検証により、検証効率と信頼性の両立を図る。