研究課題/領域番号 |
22KJ1437
|
補助金の研究課題番号 |
22J21742 (2022)
|
研究種目 |
特別研究員奨励費
|
配分区分 | 基金 (2023) 補助金 (2022) |
応募区分 | 国内 |
審査区分 |
小区分60050:ソフトウェア関連
|
研究機関 | 総合研究大学院大学 |
研究代表者 |
郡 茉友子 総合研究大学院大学, 複合科学研究科, 特別研究員(DC1)
|
研究期間 (年度) |
2023-03-08 – 2025-03-31
|
研究課題ステータス |
交付 (2023年度)
|
配分額 *注記 |
2,500千円 (直接経費: 2,500千円)
2024年度: 800千円 (直接経費: 800千円)
2023年度: 800千円 (直接経費: 800千円)
2022年度: 900千円 (直接経費: 900千円)
|
キーワード | 形式検証 / 不動点 / 圏論 |
研究開始時の研究の概要 |
データドリブン検証手法群を圏論と不動点理論をもちいて抽象化し統一的理論をつくるとともに、それを生かして新アルゴリズムの導出を目指す。検証問題は不動点理論と深いつながりがあり、また圏論による検証手法の抽象化はよりよい手法の考案につながる。また、データドリブン検証手法は高い実効性により近年注目を集めているが、基礎理論が不在でヒューリスティクス的な立ち位置に置かれがちだった。これらを踏まえ、本研究では応用上重要なデータドリブン検証手法を対象として、基礎理論を構築しよりよい手法を考案する。
|
研究実績の概要 |
本研究ではデータドリブン検証手法群を圏論と不動点理論をもちいた抽象理論の樹立と、それを生かして新アルゴリズムを導出することを目指している。 令和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など他のデータドリブン検証手法についても調査を行い、抽象理論の樹立を目指す予定である。
|