ADCL：用于约束Horn子句的加速驱动子句学习
摘要：约束角褶线（CHCs）经常用于自动程序验证。因此，证明CHCs的可满足性的技术是一个非常活跃的研究领域。另一方面，用于计算循环的N倍闭包的公式的加速技术已成功用于静态程序分析。我们展示了如何利用加速技术，在解决方案证明中避免使用递归CHC产生重复的推导，从而大大减少了证明的长度。这个想法产生了一种新的用于证明CHC的可满足性的演算法，称为加速驱动子句学习（ADCL）。我们在我们的工具LoAT中实现了这个新的演算法，并与其他最先进的工具进行了经验评估。
作者：Florian Frohn, J"urgen Giesl
论文ID：2303.01827
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-17