| 研究課題/領域番号 |
15K00093
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 電子情報学系, 教授 (70263506)
|
|---|
| 研究分担者 |
櫻井 孝平 金沢大学, 電子情報学系, 助教 (80597021)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 組込みアセンブリプログラム / ソフトウェアモデル検査 / プログラム解析 / SMT / 抽象化精錬 |
|---|
| 研究実績の概要 |
平成28年度は以下を行った。
（１）アセンブリプログラムから検証モデル（Kripke構造）を構築する際に、状態爆発を抑制して、モデル検査するシステムを実装して、多数の組込みアセンブリプログラムで計算機実験を行った。
また、その成果を英語ジャーナルに投稿して、条件付き採録であった。その論文の追加修正を行い、現在、最終判定待ちである。
（２）SMTソルバによるアセンブリプログラムの演繹的検証手法及びInterpolationによる精錬手法を改善中である。実装は平成29年度に行う予定である。その手法の特徴は以下である。①データ抽象化により、抽象モデルを構築する。②反例発見後は反例解析を行い、実反例があれば、CraigのInterpolationは効率が悪いので、RyndonのInterpolationを用いる。そのことを机上で実証した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
抽象化精錬において、反例発見後は反例解析を行い、実反例があれば、CraigのInterpolationで精錬述語を発見すると、効率が悪いことが判明した。そこで、それに代わる効率の良い方法を見つけるのに時間を要したためにやや遅れた。
しかし、RyndonのInterpolationという効率のよい方法を発見した。また、そのことを実例を用いて、机上で実証した。
|
| 今後の研究の推進方策 |
平成28年度までに、以下の手法を開発した。
①データ抽象化により、抽象モデルを構築する。
②反例発見後は反例解析を行い、実反例があれば、CraigのInterpolationは効率が悪いので、RyndonのInterpolationを用いる。
今後は、Uppsala大学のPhilipp RümmerのPrincess（Theorem Proving in First-Order Logic modulo Linear Integer Arithmetic）などの適当な定理証明系を利用して、検証システムを実装する。
|
