Lifting CDCL to Template-based Abstract Domains for Program Verification

TL;DR

This paper introduces ACDLP, a novel extension of CDCL to template polyhedra for program verification, achieving significant efficiency and precision improvements over existing tools.

Contribution

It presents the first instantiation of CDCL with a template polyhedra domain, generalizing Boolean CDCL to richer program analysis abstractions.

Findings

Achieves 100x reduction in decisions, propagations, conflicts compared to CBMC.

Runs 1.5 times faster than CBMC in verification tasks.

Solves twice as many benchmarks as Astree with higher precision.

Abstract

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.