Name
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 with 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 implemented ACDLP for automatic bounded safety verification of C programs. We evaluate the performance of our analyser by comparing with CBMC, which uses Boolean 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. |
Year | Venue | DocType |
|---|---|---|
2017 | ATVA | Conference |
Volume | Citations | PageRank |
abs/1707.02011 | 0 | 0.34 |
References | Authors | |
14 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rajdeep Mukherjee | 1 | 11 | 3.40 |
| Peter Schrammel | 2 | 134 | 19.10 |
| Leopold Haller | 3 | 127 | 6.93 |
| Daniel Kroening | 4 | 3084 | 187.60 |
| Thomas F. Melham | 5 | 384 | 35.63 |