自动化不可实现性逻辑：面向无限程序集的 Hoare 风格证明合成

对（可能无限的）程序集中所有成员的自动化验证在程序合成以及动态加载代码、并发代码和语言属性的验证中具有潜在的应用价值。现有的程序集验证技术在范围上存在局限，无法创建或使用关于程序集的可解释或可重用信息。其后果是无法从一个验证问题中学习到可用于另一个问题的任何信息。由 Kim 等人提出的不可实现性逻辑（UL），作为第一个用于证明由正则树语法定义的程序集属性的 Hoare 风格证明系统，提供了一个可以表达和使用可重用见解的理论框架。具体而言，UL 具有非终结符摘要——表征递归非终结符的归纳事实（类似于 Hoare 逻辑中的过程摘要）。在这项工作中，我们设计了第一个 UL 证明合成算法，并实现为 Wuldo。具体来说，我们通过以完全语法导向的方式计算证明结构，将决定如何应用 UL 规则的问题与合成/检查非终结符摘要的问题解耦。我们表明，当提供非终结符摘要时，Wuldo 能够表达并证明现有工具无法触及的验证问题，包括确立无限多程序在无限多输入上的行为。在某些情况下，Wuldo 甚至能够合成必要的非终结符摘要。此外，Wuldo 可以在验证查询之间重用先前已证明的非终结符摘要，使得验证速度是从头证明摘要时的 1.96 倍。