| 研究課題/領域番号 |
23K20380
|
|---|
| 補助金の研究課題番号 |
20H04162 (2020-2023)
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 基金 (2024)
補助金 (2020-2023) |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東北大学 (2024)
筑波大学 (2020-2023) |
|---|
研究代表者 |
海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
|
|---|
| 研究分担者 |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
17,030千円 (直接経費: 13,100千円、間接経費: 3,930千円)
2024年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2023年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2022年度: 3,640千円 (直接経費: 2,800千円、間接経費: 840千円)
2021年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2020年度: 4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
|
|---|
| キーワード | プログラム合成 / プログラム検証 / 時相的仕様 / 関係的仕様 / 不動点論理 / de Morgan双対性 / CHC optimization / shift0/reset0 / 循環証明 / 述語制約解消 |
|---|
| 研究開始時の研究の概要 |
高度情報化社会において、日常業務の自動化から社会基盤を支えるシステム開発まで、様々な場面でプログラミングの重要性が増している。本研究では、ミッションクリティカルシステムの一部としての利用にも耐える高信頼・高効率のプログラムを、必ずしもプログラミングや形式手法の知識を持たないユーザが、少ない労力で得ることが可能な世界の実現を目指し、プログラム検証・合成のための理論構築およびツールの研究・開発を行う。
|
| 研究実績の概要 |
本研究では、ミッションクリティカルシステムの一部としての利用にも耐える高信頼・高効率のプログラムを、必ずしもプログラミングや形式手法の知識を持たないユーザが、少ない労力で得ることが可能な世界の実現を目指し、プログラム検証・合成のための理論構築およびツールの研究・開発を行う。特にオブジェクト指向・関数型言語で記述される高レベルプログラムと時相的・関係的仕様を検証・合成の対象とし、我々が世界をリードする検証理論（リファインメント型・動的論理・不動点論理）・ツールを形式言語理論に基づき発展させることによりプログラム合成も可能とする。
本年度は、1階不動点論理の妥当性判定をde Morgan双対性に基づき行うソルバ MuVal および制約充足問題のクラス CHC を最適化問題に一般化した CHC optimization を解くソルバ OptPCSat を研究・開発した。MuVal は reactive synthesis と呼ばれる時相論理で記述された仕様からプログラムを合成する問題に、OptPCSat は unrealizability checkingと呼ばれる与えられた仕様を満たすプログラムが存在しないことを判定する問題に適用可能である。さらに、関数型言語 OCaml のための検証器 RCaml を拡張し、コントロールオペレータshift0/reset0 を用いた高階関数型プログラムの時相的仕様検証を世界で初めて実現した。これらの成果をまとめた3本の論文はすべて、プログラミング言語分野のトップ国際会議である POPL 2023 で発表した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
研究実績の概要で述べたとおり、不動点論理のde Morgan双対性を利用した妥当性判定やCHC optimization、shift0/reset0を用いたプログラムの時相仕様検証といった当初の計画を発展させた成果を得て、最高峰の国際会議で発表を行うことができたため。
|
| 今後の研究の推進方策 |
今後も計画通り研究を推進すると同時に計画を超えて得られた成果についても深化させる。具体的には、RCaml をshift0/reset0以外のコントロールオペレータ、例えば control0/prompt0 や代数エフェクト・ハンドラに拡張したり、CHC optimization を一般化して不動点論理の最適化問題を扱ったり、不動点論理の妥当性判定器を、game solving や bisimulation verification といったこれまで扱って来なかった問題に応用する。
|
