Title: Lifting CDCL to Template-based Abstract Domains for Program Verification,
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.