程序验证的自动HFL(Z)有效性检查
摘要：自动检查具有不动点运算符和整数的HFL（Z）公式的有效性的方法。结合Kobayashi等人提出的将高阶程序验证简化为HFL(Z)有效性检查的方法，我们的方法为高阶函数程序的任意时间属性提供了全自动、统一的验证方法，该方法可在模式μ-演算中表示，包括终止、非终止、公平终止、公平非终止以及分支时间属性。我们已经实现了我们的方法并获得了有希望的实验结果。
作者：Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada
论文ID：2203.07601
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-12-12