Synthesis of High-Level Programs from Temporal and Relational Specifications
Synthesis of High-Level Programs from Temporal and Relational Specifications
批准号:
20H04162
负责人:
海野 広志
金额:
$10.9万
依托单位:
依托单位国家:
日本
项目类别:
Grant-in-Aid for Scientific Research (B)
财政年份:
2020
资助国家:
日本
项目状态:
未结题
起止时间:
2020-04-01 至 2025-03-31
中文摘要
点击翻译按钮获取中文摘要
英文摘要
本研究では、ミッションクリティカルシステムの一部としての利用にも耐える高信頼・高効率のプログラムを、必ずしもプログラミングや形式手法の知識を持たないユーザが、少ない労力で得ることが可能な世界の実現を目指し、プログラム検証・合成のための理論構築およびツールの研究・開発を行う。特にオブジェクト指向・関数型言語で記述される高レベルプログラムと時相的・関係的仕様を検証・合成の対象とし、我々が世界をリードする検証理論(リファインメント型・動的論理・不動点論理)・ツールを形式言語理論に基づき発展させることによりプログラム合成も可能とする。本年度は、1階不動点論理の循環証明およびmaximally conservative interpolationに基づくソフトウェアモデル検査の基礎理論構築を行い、その成果をプログラミング言語分野のトップ国際会議であるPOPL 2022で発表した。
期刊论文(11)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
Constraint-Based Relational Verification
基于约束的关系验证
DOI:
10.1007/978-3-030-81685-8_35
发表时间:
2021
期刊:
Proceedings of CAV 2021, Springer LNCS
影响因子:
--
作者:
[Unno Hiroshi, Terauchi Tachio, Koskinen Eric]
通讯作者:
Koskinen Eric
Complexity Analysis of Extended Regular Expression Matching
扩展正则表达式匹配的复杂度分析
DOI:
10.11309/jssst.38.2_53
发表时间:
2021
期刊:
Computer Software
影响因子:
--
作者:
[高橋和也, 南出靖彦]
通讯作者:
南出靖彦
Context-Free Grammars with Lookahead
具有前瞻功能的上下文无关语法
DOI:
10.1007/978-3-030-68195-1_16
发表时间:
2021
期刊:
International Conference on Language and Automata Theory and Applications
影响因子:
--
作者:
[高橋和也, 南出靖彦, Takayuki Miyazaki and Yasuhiko Minamide]
通讯作者:
Takayuki Miyazaki and Yasuhiko Minamide
Decision Tree Learning in CEGIS-Based Termination Analysis
基于 CEGIS 的终止分析中的决策树学习
DOI:
10.1007/978-3-030-81688-9_4
发表时间:
2021
期刊:
Proceedings of CAV 2021, Springer LNCS
影响因子:
--
作者:
[Kura Satoshi, Unno Hiroshi, Hasuo Ichiro]
通讯作者:
Hasuo Ichiro
DOI:
10.1145/3498725
发表时间:
2021-11
期刊:
Proceedings of the ACM on Programming Languages
影响因子:
--
作者:
[Takeshi Tsukada;Hiroshi Unno]
通讯作者:
Takeshi Tsukada;Hiroshi Unno
共 7 条
時相的・関係的仕様からの高レベルプログラム合成
-
批准号:23K20380
-
项目类别:Grant-in-Aid for Scientific Research (B)
-
资助金额:$2.0万
-
财政年份:2024
-
负责人:海野 広志
-
依托单位:
海外基金