| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2015: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
|
|---|
| 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.
|
