2022 Fiscal Year Annual Research Report
データドリブン検証手法の圏論・不動点理論による抽象理論確立と新アルゴリズムの導出
| Project/Area Number |
22J21742
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | The Graduate University for Advanced Studies |
|---|
Principal Investigator |
郡 茉友子 総合研究大学院大学, 複合科学研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2022-04-22 – 2025-03-31
|
| Keywords | 形式検証 / 不動点 / 圏論 |
|---|
| Outline of Annual Research Achievements |
本研究ではデータドリブン検証手法群を圏論と不動点理論をもちいた抽象理論の樹立と、それを生かして新アルゴリズムを導出することを目指している。
令和4年度はデータドリブン検証手法の一つであるIC3/PDRの抽象化を行った。束論とその不動点理論を用いて抽象化を行い、最小不動点がある値以下かどうかという非常に一般的な問題を解くアルゴリズムを擬似コードとして記述した。この抽象化されたアルゴリズムから、束などのパラメータを変えることで具体化を行うことができる。特に遷移システムに対して具体化するために、圏論の余代数とファイブレーションを用いたフレームワークを作った。これにより既存のIC3/PDR由来のアルゴリズムを統一的に扱うことができた。
理論的な結果だけでなく、擬似コードをもとにHaskellで実装を行った。型クラスを用いて抽象度を保った実装を行い、ユーザーが様々な具体化を扱えるように実装した。
以上の成果についての論文は査読付き国際会議CAV'22に採択され、口頭発表も行った。IC3/PDRに関しては抽象理論の樹立という本研究の目標を達成したといえる。
また、ピサ大学のFilippo Bonchi氏のもとで研究活動を行い、CAV'22論文で樹立した抽象理論をもとにアルゴリズムの改善に取り組んだ。抽象化によって他の手法を適用しやすくなったことを利用し、改善を行った。特に、不動点を使った検証において効果的な手法である抽象解釈を参考にした。
令和5年度は引き続き抽象化を生かしてアルゴリズムの改善を目指す予定である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の研究計画は以下の通りである。
(1)データドリブン検証手法の一つであるCEGISの抽象理論樹立(採用前~2年目)、(2) データドリブン検証手法の一つであるIC3/PDRの抽象理論樹立(採用前~2年目)、(3) 新アルゴリズムの開発と実装(2年目~3年目)。
(2)に関しては目標を達成し、CAV'22論文として成果を発表した。しかし、(1)に関しては未着手である。
|
| Strategy for Future Research Activity |
樹立したIC3/PDRの抽象理論をもとにアルゴリズムの改善および新アルゴリズムの開発と実装を行う。
IC3/PDRの抽象化として束論を使った擬似コードを作ったため、束論において検証に有効な手法を容易に適用できるようになった。これを利用しこれまででは適用が難しかった手法を検討し、適用することでアルゴリズムの改善と新アルゴリズムの開発、実装を目指す。
また、CEGISなど他のデータドリブン検証手法についても調査を行い、抽象理論の樹立を目指す予定である。
|
