Dependent refinement types and predicate constraints for program verification

点击翻译按钮获取中文摘要

無限状態プログラムの時相論理仕様の検証など様々なプログラム検証の問題を表現することのできる一階不動点論理(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)に採録された。