一句话：提出 HFL(Z) 公式有效性的自动判定方法，配合归约实现对高阶函数式程序各类时序性质的统一全自动验证。
高阶函数式程序的自动化验证长期面临可表达性与自动化程度的权衡。本文提出 HFL(Z)——带不动点算子与整数的高阶逻辑——公式有效性的自动判定方法；结合 Kobayashi 等人将高阶程序验证归约为 HFL(Z) 有效性检查的结果，该方法可对模态 mu-演算可表达的高阶函数式程序任意时序性质给出统一的全自动验证，涵盖终止、非终止、公平终止、公平非终止以及分支时序性质。作者实现了该判定方法，并取得了有前景的初步实验结果。
We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reduction from higher-order program verification to HFL(Z) validity checking, our method yields a fully automated, uniform verification method for arbitrary temporal properties of higher-order functional programs expressible in the modal mu-calculus, including termination, non-termination, fair termination, fair non-termination, and also branching-time properties. We have implemented our method and obtained promising experimental results.
@article{paperbot2097,
title = {HFL(Z) Validity Checking for Automated Program Verification},
author = {Naoki Kobayashi and Kento Tanahashi and Ryosuke Sato and Takeshi Tsukada},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571199}
}