2022 Fiscal Year Annual Research Report
Dependent refinement types and predicate constraints for program verification
| Project/Area Number |
22H03570
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2022-04-01 – 2027-03-31
|
| Keywords | プログラム検証 / 不動点論理 / 型システム / 自動定理証明 / 述語制約解消 / 代数的エフェクト |
|---|
| Outline of Annual Research Achievements |
無限状態プログラムの時相論理仕様の検証など様々なプログラム検証の問題を表現することのできる一階不動点論理(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)に採録された。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究はおおむね順調に進展している。「研究実績の概要」で述べた通り、今年度は主に一階不動点論理と述語制約に関する研究を行い成果を得た。
また、型システムに関する研究としては、代数的エフェクト(algebraic effects)のための新しい依存篩型システムや多相再帰(polymorphic recursion)に関する研究を行っており、こちらの研究もおおむね順調に進展している。
|
| Strategy for Future Research Activity |
引き続き述語制約および不動点論理に関する研究を行う。特に、今年度開発した、述語制約への帰着と不動点論理の双対性を用いた新たな不動点論理妥当性判定手法の応用および手法のさらなる深化を目指す。加えて、代数的エフェクト(algebraic effects)や多相再帰(polymorphic recursion)など型システムに関する研究を行う。
|
