2009 Fiscal Year Final Research Report
Development of an automatic safety property prover with lemma discovery based on test
| 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
|
| 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.
|
Research Products
(1 results)
