论文标题
自动HFL（Z）有效性检查程序验证
Automatic HFL(Z) Validity Checking for Program Verification
论文作者
论文摘要
我们提出了一种自动化方法，用于检查HFL（Z）公式的有效性，HFL（Z）是带有FixPoint Operators和Integers的高阶逻辑。结合Kobayashi等人从高阶程序验证到HFL（Z）有效性检查的减少，我们的方法得出了一种完全自动化的，均匀的验证方法，用于在模态MU-Calculus中表达的高阶功能程序的任意时间性能，包括终止，非终端，非终端，非终止，公平终止，公平的非终端属性和分支机构。我们已经实施了我们的方法，并获得了有希望的实验结果。
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.
