| 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)
|
|---|
| 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.
|
