| 研究課題/領域番号 |
15K00093
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 電子情報学系, 教授 (70263506)
|
|---|
| 研究分担者 |
櫻井 孝平 金沢大学, 電子情報学系, 助教 (80597021)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| 研究課題ステータス |
完了 (2017年度)
|
| 配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2017年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2016年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2015年度: 2,210千円 (直接経費: 1,700千円、間接経費: 510千円)
|
|---|
| キーワード | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 抽象化精錬 / ＳＭＴ / 定理証明 / 動的プログラム解析 / SMT / プログラム解析 |
|---|
| 研究成果の概要 |
研究成果は以下の2つに大別できる．
（1）動的プログラム解析の枝刈りと抽象化，実行時間見積もりによる最小なモデル構築器（アセンブリプログラムから割込み処理が埋め込まれた最小モデルを構築する）を作成した．
（2）抽象化精錬(CEGAR)型ＳＭＴモデル検査手法を開発した．このモデル検査手法はＳＭＴによる述語抽象化、ＳＭＴ有界モデル検査、ＳＭＴによる反例解析器、ＳＭＴソルバによるInterpolationを用いた精錬述語の生成からなる．なお、ＳＭＴソルバとして、種々のInterpolationをサポートしているUppsala大学のPrincessを用いた．
|
