Large scale verification of higher-order programs

2016 Fiscal Year Final Research Report

• Project/Area Number: 26330082
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: Terauchi Tachio 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (70447150)
• Project Period (FY): 2014-04-01 – 2017-03-31
• Keywords: プログラム検証 / モデル検査 / 高階関数 / 述語論理 / 型システム / 抽象詳細化 / 時相論理

Outline of Final Research Achievements

The goal of the research is to advance the state of the art on automatic verification techniques of higher-order functional programs. We have especially focused on the techniques based on software model checking via dependent type inference, that has gained popularity in the recent years.

The main contributions of the research are as follows: 1.) New, improved abstraction refinement methods (abstraction refinement is a technique used in software model checking), 2.) New automatic methods for verification of temporal properties (such as termination and liveness) of higher-order functional programs.

Free Research Field

ソフトウェア