AI時代を見据えたプログラム検証技術
本ページは、
JSPS科学研究費補助金 基盤研究S 「AI時代を見据えたプログラム検証技術」（科研費番号：20H05703, 2020-2024年度）
の補助をうけた研究プロジェクトについての紹介です。
本プロジェクトの前身である
基盤研究S 「高階モデル検査の深化と発展」（平成27〜31年度、研究代表者：小林直樹）のプロジェクトについては
こちらをご覧ください
新着ニュース
- 2022.1: 塚田、海野による論文がPOPL 2022で発表されました。
- 2022.1: 小林がPEPM 2022で招待講演を行いました。
- 2019.9: 本プロジェクトがJSPS科学研究費補助金 基盤研究Sに採択されました。
本研究プロジェクトの概要
プログラム検証とは、プログラムが正しく振る舞うかどうかを実行前に網羅的に検証する技術であり、ソフトウェアの信頼性向上のために欠かせないものです。本研究課題では、近年の機械学習技術の台頭とそれに伴うコンピュータによって制御されたシステムの社会への普及を踏まえ、（１）小林らがこれまで研究を進めてきた高階モデル検査などの自動プログラム検証技術や理論をさらに発展させるとともに、（２）プログラム検証技術のさらなる飛躍のために機械学習技術を活用し、さらに（３）機械学習技術の台頭に伴うソフトウェアの質と量の変化に対応するための、新たなプログラム検証技術の確立を目指しています。
本プロジェクトの成果として得られたツール群
本プロジェクトの一環で開発・発展させた検証ツール等へのリンクです。
プロジェクトのメンバー
- 研究代表者：小林直樹（東京大学）
- 研究分担者：五十嵐 淳（京都大学），
海野 広志（筑波大学），佐藤 一誠（東京大学），吉仲 亮（東北大学），
塚田 武志（千葉大学），佐藤 亮介（東京大学），関山 太朗（NII）
問い合わせ先：小林（
）