University of Sussex
Browse
paper.pdf (308.21 kB)

Lifting CDCL to template-based abstract domains for program verification

Download (308.21 kB)
conference contribution
posted on 2023-06-09, 07:30 authored by Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham
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.

History

Publication status

  • Published

File Version

  • Accepted version

Journal

Automated Technology for Verification and Analysis

Publisher

Springer

Page range

307-326

Event name

International Symposium on Automated Technology for Verification and Analysis

Event location

Pune, India

Event type

conference

Event date

3-6 October 2017

ISBN

9783319681665

Series

Lecture notes in computer science

Department affiliated with

  • Informatics Publications

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2017-08-02

First Open Access (FOA) Date

2017-10-23

First Compliant Deposit (FCD) Date

2017-08-01

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC