研究課題
本研究ではデータドリブン検証手法群を圏論と不動点理論をもちいた抽象理論の樹立と、それを生かして新アルゴリズムを導出することを目指している。令和4年度はデータドリブン検証手法の一つであるIC3/PDRの抽象化を行った。束論とその不動点理論を用いて抽象化を行い、最小不動点がある値以下かどうかという非常に一般的な問題を解くアルゴリズムを擬似コードとして記述した。この抽象化されたアルゴリズムから、束などのパラメータを変えることで具体化を行うことができる。特に遷移システムに対して具体化するために、圏論の余代数とファイブレーションを用いたフレームワークを作った。これにより既存のIC3/PDR由来のアルゴリズムを統一的に扱うことができた。理論的な結果だけでなく、擬似コードをもとにHaskellで実装を行った。型クラスを用いて抽象度を保った実装を行い、ユーザーが様々な具体化を扱えるように実装した。以上の成果についての論文は査読付き国際会議CAV'22に採択され、口頭発表も行った。IC3/PDRに関しては抽象理論の樹立という本研究の目標を達成したといえる。また、ピサ大学のFilippo Bonchi氏のもとで研究活動を行い、CAV'22論文で樹立した抽象理論をもとにアルゴリズムの改善に取り組んだ。抽象化によって他の手法を適用しやすくなったことを利用し、改善を行った。特に、不動点を使った検証において効果的な手法である抽象解釈を参考にした。令和5年度は引き続き抽象化を生かしてアルゴリズムの改善を目指す予定である。
2: おおむね順調に進展している
当初の研究計画は以下の通りである。(1)データドリブン検証手法の一つであるCEGISの抽象理論樹立(採用前~2年目)、(2) データドリブン検証手法の一つであるIC3/PDRの抽象理論樹立(採用前~2年目)、(3) 新アルゴリズムの開発と実装(2年目~3年目)。(2)に関しては目標を達成し、CAV'22論文として成果を発表した。しかし、(1)に関しては未着手である。
樹立したIC3/PDRの抽象理論をもとにアルゴリズムの改善および新アルゴリズムの開発と実装を行う。IC3/PDRの抽象化として束論を使った擬似コードを作ったため、束論において検証に有効な手法を容易に適用できるようになった。これを利用しこれまででは適用が難しかった手法を検討し、適用することでアルゴリズムの改善と新アルゴリズムの開発、実装を目指す。また、CEGISなど他のデータドリブン検証手法についても調査を行い、抽象理論の樹立を目指す予定である。
すべて 2022 その他
すべて 国際共同研究 (1件) 雑誌論文 (1件) (うち査読あり 1件、 オープンアクセス 1件) 学会発表 (3件) (うち国際学会 1件、 招待講演 1件)
Computer Aided Verification. CAV 2022. Lecture Notes in Computer Science.
巻: vol 13371 ページ: 235～256
10.1007/978-3-031-13185-1_12
