NISTEP注目科学技術 - 2023_E375
概要
定理証明支援系によるソフトウェアの正当性の証明
キーワード
高信頼ソフトウェア / 定理証明支援系 / 型システム
| ID | 2023_E375 |
|---|---|
| 調査回 | 2023 |
| 注目/兆し | 注目 |
| 所属機関 | 大学 |
| 専門分野 | 情報通信 |
| 専門度 | 高 |
| 実現時期 | 10年以降 |
| 分析データ 推定科研費審査区分（中区分） | 60 （情報科学、情報工学） |
| 分析データ クラスタ | 1 （データサイエンス/情報数学・離散数学・数値計算） |
研究段階
大きなソフトウェアに対する証明はいくつか存在するが、開発に多大な人的・時間的コストがかかる。
インパクト
定理証明支援系は証明の正しさを保証するため、それによって正当性が示されたソフトウェアは必ず仕様通りに動作する。
必要な要素
証明の記述に対するサポート（必要な補題の提示など）