| 研究課題/領域番号 |
20H04162
|
|---|
| 配分区分 | 補助金 |
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究分担者 |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| キーワード | プログラム検証 / 関係的仕様 / 述語制約解消 |
|---|
| 研究実績の概要 |
本研究では、ミッションクリティカルシステムの一部としての利用にも耐える高信頼・高効率のプログラムを、必ずしもプログラミングや形式手法の知識を持たないユーザが、少ない労力で得ることが可能な世界の実現を目指し、プログラム検証・合成のための理論構築およびツールの研究・開発を行う。特にオブジェクト指向・関数型言語で記述される高レベルプログラムと時相的・関係的仕様を検証・合成の対象とし、我々が世界をリードする検証理論（リファインメント型・動的論理・不動点論理）・ツールを形式言語理論に基づき発展させることによりプログラム合成も可能とする。本年度は、特に関係的仕様の自動検証を実現するため、CHCという形式検証のための制約言語を拡張したpfwCSP制約言語を導入し、関係的仕様検証問題からpfwCSPへの健全かつ完全な帰着法も与えた。さらに、pfwCSP制約を解消するためにテンプレートに基づく解の合成法、決定木学習に基づく合成法、ニューラルネットワークに基づく合成法の3つを提案し、研究成果を3本の論文にまとめた。そのうちの前者2本はシステム検証のトップ国際会議であるCAV 2021に採録されている。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究実績の概要で述べたとおり、関係的仕様検証の自動化を実現するための理論構築からツール開発まで完了している。それらの成果はトップ国際会議2本を含む3本の論文として発表している。
|
| 今後の研究の推進方策 |
今後も計画通り研究を推進する。ツールの完成度を高めるのに加えて、導入した制約言語の新しい応用についても検討する。
|
