项目标书摘要:Outline of Research at the Start:AIを用いたソフトウェアは,AIモジュールのブラックボックス性のために従来の形式検証手法をそのまま適用することが困難である.このようなソフトウェア安全性を向上させるための形式検証手法の確立に向けて,内部動作が明らかではなく,期待される動作の形式的仕様記述も困難であるモジュールを含むシステムの動作を検証するための手法を研究する.より具体的には,AIモジュールを含むソフトウェアへの適用を志向した,形式的仕様が与えられていないブラックボックスな部品を含むソフトウェアのための形式検証手法を研究する。