paper.pdf (308.21 kB)
Lifting CDCL to template-based abstract domains for program verification
conference contribution
posted on 2023-06-09, 07:30 authored by Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom MelhamThe 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.
History
Publication status
- Published
File Version
- Accepted version
Journal
Automated Technology for Verification and AnalysisPublisher
SpringerExternal DOI
Page range
307-326Event name
International Symposium on Automated Technology for Verification and AnalysisEvent location
Pune, IndiaEvent type
conferenceEvent date
3-6 October 2017ISBN
9783319681665Series
Lecture notes in computer scienceDepartment affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2017-08-02First Open Access (FOA) Date
2017-10-23First Compliant Deposit (FCD) Date
2017-08-01Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC