Study on Software Verification Methods Using Program Transformation Handling Infinite Terms
| Project/Area Number |
24500171
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | Nagoya Institute of Technology |
|---|
Principal Investigator |
Seki Hirohisa 名古屋工業大学, 工学(系)研究科(研究院), 教授 (90242908)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000)
Fiscal Year 2014: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2013: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2012: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | 探索・論理・推論アルゴリズム / 計算論理 / プログラム推論 / プログラム変換 / システム検証 |
|---|
| Outline of Final Research Achievements |
The overall objective of this research is to develop a computational-logic based methodology for verifying software such as reactive systems using transformational verification methods; we use logic programs to represent a given system and reason about its properties. We have obtained the following three main results:
(1) We have proposed a reasoning method for co-logic programs. We have shown by some examples that it can be used for verifying some given specifications in a succinct way. (2) We have proposed an extended framework for co-logic programs, and shown that it is applicable to the model checking problem for CTL temporal logic formulas. (3) We have proposed a new method for pattern mining which will become a basis for specification discovery.
|
Report
(5 results)
Research Products
(12 results)
