関数型言語のための統一的検証基盤構築に向けて

• 研究課題/領域番号: 25K15052
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60050:ソフトウェア関連
• 研究機関: 東京農工大学
• 研究代表者: 佐藤 亮介 東京農工大学, 学内共同利用施設等, 准教授 (10804677)
• 研究期間 (年度): 2025-04-01 – 2029-03-31
• 研究課題ステータス: 交付 (2025年度)
• 配分額: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円); 2028年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2027年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2026年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2025年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円)
• キーワード: ソフトウェアの安全性 / 形式的検証 / 関数型言語 / 検証基盤

研究開始時の研究の概要

ソフトウェアが社会の至る所で用いられるようになり、その安全性が非常に重要になっている。ソフトウェアの安全性を形式的に保証するため様々な手法が提案されており、それらの手法に基づいた検証器も積極的に開発、使用されている。しかしながら、プログラミング言語も検証手法も次々と新しいものが提案されるため、特定の言語に対して特定の検証手法を用いた検証器が独立に開発されている状況となっている。本研究課題では、様々な言語に対する検証問題を帰着可能な中間言語、および、その中間言語で書かれたプログラムの安全性や正当性を高精度かつ効率的に検証する手法を開発する。