データドリブン検証手法の圏論・不動点理論による抽象理論確立と新アルゴリズムの導出
Project/Area Number |
22KJ1437
|
Project/Area Number (Other) |
22J21742 (2022)
|
Research Category |
Grant-in-Aid for JSPS Fellows
|
Allocation Type | Multi-year Fund (2023) Single-year Grants (2022) |
Section | 国内 |
Review Section |
Basic Section 60050:Software-related
|
Research Institution | The Graduate University for Advanced Studies |
Principal Investigator |
郡 茉友子 総合研究大学院大学, 複合科学研究科, 特別研究員(DC1)
|
Project Period (FY) |
2023-03-08 – 2025-03-31
|
Project Status |
Granted (Fiscal Year 2023)
|
Budget Amount *help |
¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 2024: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2023: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2022: ¥900,000 (Direct Cost: ¥900,000)
|
Keywords | 形式検証 / 不動点 / 圏論 |
Outline of Research at the Start |
データドリブン検証手法群を圏論と不動点理論をもちいて抽象化し統一的理論をつくるとともに、それを生かして新アルゴリズムの導出を目指す。検証問題は不動点理論と深いつながりがあり、また圏論による検証手法の抽象化はよりよい手法の考案につながる。また、データドリブン検証手法は高い実効性により近年注目を集めているが、基礎理論が不在でヒューリスティクス的な立ち位置に置かれがちだった。これらを踏まえ、本研究では応用上重要なデータドリブン検証手法を対象として、基礎理論を構築しよりよい手法を考案する。
|
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など他のデータドリブン検証手法についても調査を行い、抽象理論の樹立を目指す予定である。
|
Report
(1 results)
Research Products
(5 results)