提升CDCL到基于模板的抽象域的程序验证
Lifting CDCL to Template-based Abstract Domains for Program Verification
摘要：
冲突驱动子句学习（CDCL）在布尔可满足性方面的成功启发了其他领域的采用。我们提出了一种新的提升CDCL的程序分析称为抽象冲突驱动的学习程序（ACDLP）。ACDLP在模型搜索和冲突分析之间交替，模型搜索使用约束传播执行过近似推理，冲突分析使用启发式选择执行欠近似溯因。我们将模型搜索和冲突分析算法实例化到模板多面体的抽象域，严格地将CDCL从布尔格推广到更丰富的格结构。我们的模板多面体可以表示程序变量上的区间、八边形和受限多面体约束。我们已经实现了ACDLP的自动边界安全验证的C程序。我们通过与CBMC（使用CDCL）和Astree（一种商业摘要解释工具）的比较来评估我们的分析器的性能。我们观察到两个数量级的决策，传播和冲突的数量减少，以及在运行时的1.5倍加速相比，CBMC。与Astree相比，ACDLP解决了两倍多的基准测试，并且具有更高的精度。这是CDCL的第一个实例化与模板多面体抽象域。
英文摘要：
The success of Conflict Driven Clause Learning (CDCL) for Boolean satisfiability has inspired adoption in other domains. We present a novel lifting of CDCL to program analysis called Abstract Conflict Driven Learning for Programs (ACDLP). ACDLP alternates between model search, which performs over-approximate deduction with constraint propagation, and conflict analysis, which performs under-approximate abduction with heuristic choice. We instantiate the model search and conflict analysis algorithms to an abstract domain of template polyhedra, strictly generalizing CDCL from the Boolean lattice to a richer lattice structure. Our template polyhedra can express intervals, octagons and restricted polyhedral constraints over program variables. We have imple- mented ACDLP for automatic bounded safety verification of C programs. We evaluate the performance of our analyser by comparing with CBMC, which uses CDCL, and Astree, a commercial abstract interpretation tool. We observe two orders of magnitude reduction in the number of decisions, propagations, and conflicts as well as a 1.5x speedup in runtime compared to CBMC. Compared to Astree, ACDLP solves twice as many benchmarks and has much higher precision. This is the first instantiation of CDCL with a template polyhedra abstract domain.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
