データドリブン検証手法の圏論・不動点理論による抽象理論確立と新アルゴリズムの導出

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

本研究ではデータドリブン検証手法群を圏論と不動点理論をもちいた抽象理論の樹立と、それを生かして新アルゴリズムを導出することを目指している。令和4年度はデータドリブン検証手法の一つであるIC3/PDRの抽象化を行った。束論とその不動点理論を用いて抽象化を行い、最小不動点がある値以下かどうかという非常に一般的な問題を解くアルゴリズムを擬似コードとして記述した。この抽象化されたアルゴリズムから、束などのパラメータを変えることで具体化を行うことができる。特に遷移システムに対して具体化するために、圏論の余代数とファイブレーションを用いたフレームワークを作った。これにより既存のIC3/PDR由来のアルゴリズムを統一的に扱うことができた。理論的な結果だけでなく、擬似コードをもとにHaskellで実装を行った。型クラスを用いて抽象度を保った実装を行い、ユーザーが様々な具体化を扱えるように実装した。以上の成果についての論文は査読付き国際会議CAV'22に採択され、口頭発表も行った。IC3/PDRに関しては抽象理論の樹立という本研究の目標を達成したといえる。また、ピサ大学のFilippo Bonchi氏のもとで研究活動を行い、CAV'22論文で樹立した抽象理論をもとにアルゴリズムの改善に取り組んだ。抽象化によって他の手法を適用しやすくなったことを利用し、改善を行った。特に、不動点を使った検証において効果的な手法である抽象解釈を参考にした。令和5年度は引き続き抽象化を生かしてアルゴリズムの改善を目指す予定である。