发表机构
EPFL; Microsoft Research（洛桑联邦理工学院; 微软研究院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文指出SMT求解器中量词实例化的深度记账非合流导致结果不稳定，提出一种稳定的新记账方法，在Z3中实现，使Mariposa基准不稳定核心的结果不稳定性降低94%且无性能回退。
AI 中文摘要
SMT求解器使自动化验证变得便捷。与此同时，求解器存在不稳定性问题，即对输入的看似无关紧要的改动可能导致先前快速生成的证明失败或超时。本文针对程序验证背景下结果不稳定性（即unsat/unknown波动）的一个常见原因进行了研究。我们证明，为使量词实例化实用化并在多个最先进的SMT求解器中实现的生成（即深度）记账是非合流的（即易于发散），这导致了不稳定性。随后，我们解决了这一缺陷，并开发了一种稳定的新记账方法。新方法通过从抽象的合流求解器模型到我们在Z3中的实现的一系列精化得到了论证。我们的实证评估表明，我们的实现将Mariposa基准不稳定核心中的结果不稳定性降低了94%，且未导致性能回退。
英文摘要
SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously quickly produced proof to fail or time out. This paper addresses a common cause of outcome instability (i.e., unsat/unknown fluctuations) in the context of program verification. We demonstrate that the generation (i.e., depth) accounting used to make quantifier instantiation practical and implemented in multiple state-of-the-art SMT solvers is non-confluent (i.e., prone to divergence), and that this leads to instability. We then address this deficiency and develop a new accounting method that is stable. The new method is justified using a sequence of refinements from an abstract, confluent solver model all the way to our implementation in Z3. Our empirical evaluation demonstrates that our implementation reduces outcome instability by 94% in the unstable core of the Mariposa benchmark without leading to performance regressions.
