Program Verification Methods based on Context-Moving Transformation and Higher-Order Rewriting Theory

2018 Fiscal Year Final Research Report

• Project/Area Number: 16K00091
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Tohoku University
• Principal Investigator: KIKUCHI Kentaro 東北大学, 電気通信研究所, 助教 (40396528)
• Co-Investigator(Kenkyū-buntansha): 青戸 等人 新潟大学, 自然科学系, 教授 (00293390)
• Project Period (FY): 2016-04-01 – 2019-03-31
• Keywords: 書き換えシステム / プログラム検証

Outline of Final Research Achievements

We conducted research to develop new methods for program verification based on rewriting techniques. The main results of this research are summarised as follows:
(1) Concerning rewriting systems with variable binding, we obtained several new conditions on confluence of nominal rewriting systems and other related systems. Also, we have taken part in the development of automated confluence and termination provers for versions of higher-order rewriting systems, and achieved excellent results in international competitions.
(2) Through observations on inductionless induction methods in rewriting systems without the sufficient completeness property, we developed a new verification method that is applicable to programs including those expressions which induce non-terminating computation such as infinite lists.

Free Research Field

プログラム理論

Academic Significance and Societal Importance of the Research Achievements

束縛変数を伴う書き換えシステムに対する合流性や停止性についての研究及びその成果は、従来の第一階項書き換えシステムに基づく帰納的定理証明手法である潜在帰納法および書き換え帰納法を、高階項に対する書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。また、十分完全性を持たない書き換えシステムにおける潜在帰納法についての研究及びその成果は、入力によって計算が停止しない様々なプログラムに対する検証手法を開発するにあたって重要になると考えられる。これらの成果を利用したプログラム及びプログラミング言語に対する検証手法は、ソフトウェアの信頼性を向上させる技術として役立つことが期待できる。