Lifting CDCL to template-based abstract domains for program verification

DOI10.1007/978-3-319-68167-2_21MaRDI QIDQ5096092zbMATH OpenOpenAlexFDO

Authors Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham

Publication date 12 August 2022

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1707.02011, http://sro.sussex.ac.uk/id/eprint/69532/1/paper.pdf

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational learning theory (68Q32) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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.

Recommendations

• Abstract conflict driven learning
• Logic for Programming, Artificial Intelligence, and Reasoning
• Deciding floating-point logic with abstract conflict driven clause learning
• Fast polyhedra abstract domain
• Conflict-driven conditional termination

Cited in

(3)

• Bridging the Gap: Automatic Verified Abstraction of C
• Abstract domains for reordering CLP(RLin) programs
• Information Exchange Between Over- and Underapproximating Software Analyses

This page was built for publication: Lifting CDCL to template-based abstract domains for program verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5096092)