論理制約付き項書換えに関する余帰納法に基づくプログラム検証法の開発

• 研究課題/領域番号: 24K02900
• 研究種目: 基盤研究(B)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60010:情報学基礎論関連; 小区分60020:数理情報学関連; 合同審査対象区分:小区分60010:情報学基礎論関連、小区分60020:数理情報学関連
• 研究機関: 名古屋大学
• 研究代表者: 西田 直樹 名古屋大学, 情報学研究科, 准教授 (00397449)
• 研究分担者: 松原 豊 名古屋大学, 情報学研究科, 准教授 (30547500) ; 中澤 巧爾 名古屋大学, 情報学研究科, 准教授 (80362581)
• 研究期間 (年度): 2024-04-01 – 2029-03-31
• 研究課題ステータス: 交付 (2024年度)
• 配分額: 18,460千円 (直接経費: 14,200千円、間接経費: 4,260千円); 2028年度: 5,200千円 (直接経費: 4,000千円、間接経費: 1,200千円); 2027年度: 5,460千円 (直接経費: 4,200千円、間接経費: 1,260千円); 2026年度: 5,590千円 (直接経費: 4,300千円、間接経費: 1,290千円); 2025年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2024年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
• キーワード: 論理制約付き項書換えシステム / プログラム変換 / 実行時エラー検証 / 到達可能性 / 循環証明

研究開始時の研究の概要

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