書換え型計算モデルへの変換を利用した実行時エラー検証技術の構築

• 研究課題/領域番号: 24KJ1240
• 研究種目: 特別研究員奨励費
• 配分区分: 基金
• 応募区分: 国内
• 審査区分: 小区分60010:情報学基礎論関連
• 研究機関: 名古屋大学
• 研究代表者: 小嶋 美咲 名古屋大学, 情報学研究科, 特別研究員(PD)
• 研究期間 (年度): 2024-04-23 – 2026-03-31
• 研究課題ステータス: 交付 (2024年度)
• 配分額: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円); 2025年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2024年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)

研究開始時の研究の概要

本研究では，書換え型計算モデルへの変換を利用した実行時エラー検証技術の構築のために，指定した実行時エラーが発生しないことを全パス到達可能性に帰着して検証する枠組みを開発する．具体的には，並行プログラムからLCTRSへの変換，プログラムと実行時エラーからLCTRSと全パス到達可能性問題への変換を提案する．そして，全パス到達可能性問題を解くための自動証明システムを循環証明の技術に基づき実現する．さらに，並行プログラムの検証では探索空間が膨大であるため，自動証明システムの効率化を図る．