| 研究課題/領域番号 |
20800082
|
|---|
| 研究種目 |
若手研究(スタートアップ)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 独立行政法人産業技術総合研究所 |
|---|
研究代表者 |
中野 昌弘 独立行政法人産業技術総合研究所, システム検証研究センター, 産総研特別研究員 (90470046)
|
|---|
| 研究期間 (年度) |
2008 – 2009
|
| 研究課題ステータス |
完了 (2009年度)
|
| 配分額 *注記 |
2,548千円 (直接経費: 1,960千円、間接経費: 588千円)
2009年度: 1,274千円 (直接経費: 980千円、間接経費: 294千円)
2008年度: 1,274千円 (直接経費: 980千円、間接経費: 294千円)
|
|---|
| キーワード | 仕様記述 / 数理論理学 / 並列分散処理 / アルゴリズム工学 / 仕様記述・仕様検証 |
|---|
| 研究概要 |
本研究では、不動点帰納法による検証能力の向上、適用可能規模の向上のため、テストに基づく発見的手法により帰納法の仮定を求め(補題発見)、従来手法では自動検証できなかった問題に対しても、自動的な検証を行えるようにすることを目的とする。SMTソルバとしてCVC3を利用して最弱事前条件計算を実装し、補題発見機能と不動点帰納法による不変性自動検証器を実装した。SMTを用いたことや補題の発見、各種手続きの効率化を図ることで、証明力の向上と数十倍程度の高速化を実現し、より規模の大きな問題であっても、自動で証明できるようになった。
|
