Lifting CDCL to template-based abstract domains for program verification

Mukherjee, Rajdeep, Schrammel, Peter, Haller, Leopold, Kroening, Daniel and Melham, Tom (2017) Lifting CDCL to template-based abstract domains for program verification. Published in: Automated Technology for Verification and Analysis. Springer (Accepted)

[img] PDF - Accepted Version
Restricted to SRO admin only

Download (315kB)

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 Astrée, 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 Astrée, ACDLP solves twice as many benchmarks and has much higher precision. This is the first instantiation of CDCL with a template polyhedra abstract domain.

Item Type: Conference Proceedings
Keywords: verification, satisfiability solving, relational domains, abstract interpretation, template polyhedra
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Q Science > QA Mathematics > QA0076 Computer software
Depositing User: Peter Schrammel
Date Deposited: 02 Aug 2017 09:35
Last Modified: 02 Aug 2017 09:35
URI: http://sro.sussex.ac.uk/id/eprint/69532

View download statistics for this item

📧 Request an update