权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Dependent refinement types and predicate constraints for program verification

用于程序验证的依赖细化类型和谓词约束

基本信息

批准号：
22H03570
负责人：
寺内多智弘
金额：
$ 10.73万
依托单位：
Waseda University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (B)
财政年份：
2022
资助国家：
日本
起止时间：
2022-04-01 至 2027-03-31
项目状态：
未结题

项目摘要

無限状態プログラムの時相論理仕様の検証など様々なプログラム検証の問題を表現することのできる一階不動点論理(first-order fixpoint logic)に関する研究を行った。特に、代表者らの先行研究で提案したpfwCSPという述語制約体系に一階不動点論理の妥当性判定を帰着する方法について研究を行った。より具体的には、一階不動点論理が持つ双対性をうまく利用することで、入力論理式とその否定の部分式に対する近似が互いの解空間を削減するために使えることに注目し、入力とその否定を同時並列に効率よく解く新たな妥当性判定の手法を提案した。この研究の成果をまとめた論文はプログラミング言語分野の最高峰の国際会議であるACM Symposium on Principles of Programming Languages(POPL)に採録され、Distingiushed Paper Awardも受賞した。加えて、後方参照(backreference)、先読み(lookahead)、後読み(lookbehind)といった拡張機能を含む拡張正規表現について、正規表現を含むプログラムに対する著名な脆弱性であるReDoS(regular expression denial of service)を修正するプログラム合成手法の研究と、拡張正規表現の形式言語理論に関する研究を行った。前者の研究成果をまとめた論文はセキュリティ分野の最高峰の国際会議であるIEEE Symposium on Security and Privacy (S&P)に採録され、後者の研究成果をまとめた論文は理論計算機科学分野の主要国際会議であるInternational Conference on Formal Structures for Computation and Deduction (FSCD)に採録された。

This paper studies the problem of time-phase logic of infinite state topology and its representation in first-order fixpoint logic. Special, representative and advanced research proposals pfwCSP, predicate constraint system, first-order fixed point logic and appropriateness determination, method and implementation The first order fixed point logic is to maintain the duality of the solution space. ACM Symposium on Principles of Programming Languages(POPL) was awarded the Distinguished Paper Award. Add, backreference, lookahead, lookbehind, and stretch functions include stretch formal expression, stretch formal expression, and stretch formal expression. The research results of the former were collected at the IEEE Symposium on Security and Privacy (S&P) and the research results of the latter were collected at the International Conference on Formal Structures for Computation and Deduction (FSCD).