Program Verification Techniques for the AI Era

点击翻译按钮获取中文摘要

研究課題全体を(A)高階モデル検査をはじめとするプログラム検証理論・技術のさらなる発展、(B)プログラム検証への機械学習技術の応用、(C)質の変化したプログラムの検証手法、の3つの課題に分けて並行して研究を進めた。2021年度の主な研究実績（一部、繰越分として2022年度に実施した成果を含む）は以下のとおり。(A)プログラム検証技術の発展：高階モデル検査の一種である高階不動点論理HFL(Z)の真偽値判定の高速化のため、一階のケースにおいて有効な手法であるPDRと循環証明との間の理論的関係を明らかにした。さらに、リスト構造を扱うプログラムの検証のために、記号オートマトン的関係という概念を新たに導入し、それに基づいてリストに関する性質の自動推論手法の改良を行った。また、並行プログラムの検証手法として、π計算と呼ばれる並行計算モデルで記述された並行プログラムの停止性を逐次プログラムの停止性に帰着する手法を考案し、実装・評価を行った。(B)プログラム検証への機械学習技術の応用：プログラム検証において鍵となるループ不変条件等の発見のためにニューラルネットワークを用いる枠組み（NeuGus: Neural Network-Guided Synthesis）を考案・実装し、不動点論理ソルバの一種であるCHCソルバHoIceに組み込んでその有効性を確認した。(C)質の変化したプログラムの検証手法： ニューラルネットワークを組み込んだソフトウェアの検証に向け、(B)のNeuGuSの枠組みを利用して、ニューラルネットワークから通常のプログラムコンポーネントを合成する手法を考案し、その有効性を確認した。また、確率付きプログラムの検証のための基礎として、確率付き高階不動点論理について研究を行い、モデル検査が決定可能なクラスを明らかにした。