2017 Fiscal Year Final Research Report
Verifying safety properties of embedded assembly program using innovative software model checking
| Project/Area Number |
15K00093
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
櫻井 孝平 金沢大学, 電子情報学系, 助教 (80597021)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 抽象化精錬 / ＳＭＴ / 定理証明 |
|---|
| Outline of Final Research Achievements |
The research outcome can be roughly divided into the following two.
(1) We have developed a minimal model constructor (constructing a minimum model with interrupt processing embedded from the assembly program) by pruning and abstraction of dynamic program analysis and execution time estimation.
(2) SMT model checking method based on Abstraction and Refinement (CEGAR) was developed. This model checking method consists of predicate abstraction by SMT, SMT bounded model check, counter-example analyzer by SMT, and refinement predicate generation using Interpolation by SMT solver. As the SMT solver, Princess of Uppsala University which supports various interpolations was used.
|
| Free Research Field |
ソフトウェア
|
