| 研究課題/領域番号 |
25K15065
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 早稲田大学 |
|---|
研究代表者 |
岸 知二 早稲田大学, 理工学術院, 教授 (30422661)
|
|---|
| 研究期間 (年度) |
2025-04-01 – 2028-03-31
|
| 研究課題ステータス |
交付 (2025年度)
|
| 配分額 *注記 |
4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2027年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2026年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2025年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
|---|
| キーワード | ソフトウェア / ソフトウェア工学 / 形式検証 / 機械学習 / 可変性管理 |
|---|
| 研究開始時の研究の概要 |
形式検証は論理に基づきシステムの正しさを厳密に確認する技術として，特に信頼性や安全性の求められる分野で使われているが，スケーラビリティに課題がある．一方，近年発達した機械学習による論理推論はスケーラブルだが統計的な手法であるため厳密解を得ることは困難である．本研究では機械学習による論理推論を，形式手法の厳密解に影響しないように援用することで，形式手法のスケーラビリティ改善を狙う．具体的には，形式検証を並列化する際に，機械学習により高速に得られる解の予測を活用し，システム記述の効果的な分割，効率的な並行検証の実行戦略の決定，最も適切な分割数の決定などを行う手法を提案しツールとして具現化する．
|
