| Project/Area Number |
20800082
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (Start-up)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
NAKANO Masahiro National Institute of Advanced Industrial Science and Technology, システム検証研究センター, 産総研特別研究員 (90470046)
|
|---|
| Project Period (FY) |
2008 – 2009
|
| Project Status |
Completed (Fiscal Year 2009)
|
| Budget Amount *help |
¥2,548,000 (Direct Cost: ¥1,960,000、Indirect Cost: ¥588,000)
Fiscal Year 2009: ¥1,274,000 (Direct Cost: ¥980,000、Indirect Cost: ¥294,000)
Fiscal Year 2008: ¥1,274,000 (Direct Cost: ¥980,000、Indirect Cost: ¥294,000)
|
|---|
| Keywords | 仕様記述 / 数理論理学 / 並列分散処理 / アルゴリズム工学 / 仕様記述・仕様検証 |
|---|
| Research Abstract |
In this research, we developed an automatic invariant prover based on fixed-point induction with lemma discovery. To improve features of automatic verification and efficiencies, we implemented the weakest precondition computation with an SMT solver : CVC3, then implemented functions of fixed-point induction and lemma discovery with the computation. Using an SMT solver and lemma discovery, it could speed up more than ten times and prove a large scale problem.
|
