Synthesis of High-Level Programs from Temporal and Relational Specifications
| Project/Area Number |
23K20380
|
|---|
| Project/Area Number (Other) |
20H04162 (2020-2023)
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Multi-year Fund (2024)
Single-year Grants (2020-2023) |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Tohoku University (2024)
University of Tsukuba (2020-2023) |
|---|
Principal Investigator |
海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
南出 靖彦 東京工業大学, 情報理工学院, 教授 (50252531)
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥17,030,000 (Direct Cost: ¥13,100,000、Indirect Cost: ¥3,930,000)
Fiscal Year 2024: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2023: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2022: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2021: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2020: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
|
|---|
| Keywords | プログラム合成 / プログラム検証 / 時相的仕様 / 関係的仕様 / 不動点論理 / 循環証明 / 述語制約解消 |
|---|
| Outline of Research at the Start |
高度情報化社会において、日常業務の自動化から社会基盤を支えるシステム開発まで、様々な場面でプログラミングの重要性が増している。本研究では、ミッションクリティカルシステムの一部としての利用にも耐える高信頼・高効率のプログラムを、必ずしもプログラミングや形式手法の知識を持たないユーザが、少ない労力で得ることが可能な世界の実現を目指し、プログラム検証・合成のための理論構築およびツールの研究・開発を行う。
|
| Outline of Annual Research Achievements |
本研究では、ミッションクリティカルシステムの一部としての利用にも耐える高信頼・高効率のプログラムを、必ずしもプログラミングや形式手法の知識を持たないユーザが、少ない労力で得ることが可能な世界の実現を目指し、プログラム検証・合成のための理論構築およびツールの研究・開発を行う。特にオブジェクト指向・関数型言語で記述される高レベルプログラムと時相的・関係的仕様を検証・合成の対象とし、我々が世界をリードする検証理論（リファインメント型・動的論理・不動点論理）・ツールを形式言語理論に基づき発展させることによりプログラム合成も可能とする。本年度は、1階不動点論理の循環証明およびmaximally conservative interpolationに基づくソフトウェアモデル検査の基礎理論構築を行い、その成果をプログラミング言語分野のトップ国際会議であるPOPL 2022で発表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要で述べたとおり、不動点論理の循環証明に基づくソフトウェアモデル検査の基礎理論を世界で初めて構築し、トップ国際会議で発表しているため。
|
| Strategy for Future Research Activity |
今後も計画通り研究を推進する。論文では安全性仕様検証問題しか扱っていないが、不動点論理によって関係的仕様・時相的仕様検証・合成問題も扱えることがわかっているため、今後はそのような問題のための循環証明探索法についても研究し、ツールの開発も行う。
|
Report
(2 results)
Research Products
(11 results)
