Verifying Software Systems using Reasoning about Programs Handling Infinite Structures

2017 Fiscal Year Final Research Report

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

Free Research Field

知能情報学