Verifying Software Systems using Reasoning about Programs Handling Infinite Structures
| Project/Area Number |
15K00305
|
|---|
| 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) |
2015-04-01 – 2018-03-31
|
| Project Status |
Completed (Fiscal Year 2017)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2017: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2016: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2015: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,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 program analysis; we use logic programs to represent a given system and a correctness property we want to prove, and then apply to a logic program encoding the system and the property to be verified, some methods for reasoning about programs such as program transformations that preserve the validity of that property. We have obtained the following three main results: (1) our verification method uses co-logic programs, and we have shown the relationship between co-logic programs and Horn mu-calculus and some applications of it. (2) We have proposed an algorithm for mining specification formulas from a sequence database of execution logs. (3) We have proposed a new method for mining patterns with quantitative constraints such as time constraints.
|
Report
(4 results)
Research Products
(13 results)
