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

Research Project

Project/Area Number	25K15052
Research Category	Grant-in-Aid for Scientific Research (C)
Allocation Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60050:Software-related
Research Institution	Tokyo University of Agriculture and Technology
Principal Investigator	佐藤亮介東京農工大学, 学内共同利用施設等, 准教授 (10804677)
Project Period (FY)	2025-04-01 – 2029-03-31
Project Status	Granted (Fiscal Year 2025)
Budget Amount *help	¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000) Fiscal Year 2028: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000) Fiscal Year 2027: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000) Fiscal Year 2026: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000) Fiscal Year 2025: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
Keywords	ソフトウェアの安全性 / 形式的検証 / 関数型言語 / 検証基盤
Outline of Research at the Start	ソフトウェアが社会の至る所で用いられるようになり、その安全性が非常に重要になっている。ソフトウェアの安全性を形式的に保証するため様々な手法が提案されており、それらの手法に基づいた検証器も積極的に開発、使用されている。しかしながら、プログラミング言語も検証手法も次々と新しいものが提案されるため、特定の言語に対して特定の検証手法を用いた検証器が独立に開発されている状況となっている。本研究課題では、様々な言語に対する検証問題を帰着可能な中間言語、および、その中間言語で書かれたプログラムの安全性や正当性を高精度かつ効率的に検証する手法を開発する。