Development of Program Verification Techniques Based on Coinduction on Logically Constrained Rewriting

• Project/Area Number: 24K02900
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60010:Theory of informatics-related; Basic Section 60020:Mathematical informatics-related; Sections That Are Subject to Joint Review: Basic Section60010:Theory of informatics-related , Basic Section60020:Mathematical informatics-related
• Research Institution: Nagoya University
• Principal Investigator: 西田 直樹 名古屋大学, 情報学研究科, 准教授 (00397449)
• Co-Investigator(Kenkyū-buntansha): 松原 豊 名古屋大学, 情報学研究科, 准教授 (30547500) ; 中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
• Project Period (FY): 2024-04-01 – 2029-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥18,460,000 (Direct Cost: ¥14,200,000、Indirect Cost: ¥4,260,000); Fiscal Year 2028: ¥5,200,000 (Direct Cost: ¥4,000,000、Indirect Cost: ¥1,200,000); Fiscal Year 2027: ¥5,460,000 (Direct Cost: ¥4,200,000、Indirect Cost: ¥1,260,000); Fiscal Year 2026: ¥5,590,000 (Direct Cost: ¥4,300,000、Indirect Cost: ¥1,290,000); Fiscal Year 2025: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
• Keywords: 論理制約付き項書換えシステム / プログラム変換 / 実行時エラー検証 / 到達可能性 / 循環証明

Outline of Research at the Start

近年，論理制約付き項書換えシステム（LCTRS）を用いたプログラム検証の研究が盛んになっている．本研究では，検証したいプログラムと性質それぞれをLCTRSとその検証問題に変換および帰着し，帰納法に基づいてその問題を解くプログラム検証法を開発する．帰着する検証問題には等価性問題および全パス到達可能性問題を採用し，その成否の検証を試みる．開発のための具体的な課題として，「等価性問題および全パス到達可能性問題の両方を扱う証明系の形式化と実装」，「等価性・実行時エラー非発生・メモリ安全性など様々な性質からLCTRSの検証問題への帰着」，「検証問題が決定可能となるプログラムと性質の特徴づけ」に取り組む．