Constrained Horn Clauses (CHCs) are widely used in automated program verification. Thus, techniques for (dis-)proving satisfiability of CHCs are a very active field of research. On the other hand, acceleration techniques for computing formulas that characterize the N-fold closure of loops have successfully been used for static program analysis. We show how to use acceleration to avoid repeated derivations with recursive CHCs in resolution proofs, which reduces the length of the proofs drastically. This idea gives rise to a novel calculus for (dis)proving satisfiability of CHCs, called Acceleration Driven Clause Learning (ADCL). We implemented this new calculus in our tool LoAT and evaluate it empirically in comparison to other state-of-the-art tools.

翻译：约束霍恩子句（CHCs）广泛应用于自动化程序验证中。因此，证明或证伪CHCs可满足性的技术是一个非常活跃的研究领域。另一方面，用于计算表征循环N次闭包的公式的加速技术已成功应用于静态程序分析。我们展示了如何利用加速技术避免在解析证明中重复推导递归CHCs，从而大幅缩短证明长度。这一思想催生了一种新颖的CHCs可满足性证明/证伪演算方法，称为加速度驱动子句学习（ADCL）。我们已在工具LoAT中实现了这一新演算，并通过经验评估将其与其他前沿工具进行了对比。