Sharpening Constraint Programming approaches for Bit-Vector Theory

Abstract : We address the challenge of developing efficient Constraint Programming-based approaches for solving formulas over the quantifier-free fragment of the theory of bitvectors (BV), which is of paramount importance in software verification. We propose CP(BV), a highly efficient BV resolution technique built on carefully chosen anterior results sharpened with key original features such as thorough domain combination or dedicated labeling. Extensive experimental evaluations demonstrate that CP(BV) is much more efficient than previous similar attempts from the CP community, that it is indeed able to solve the majority of the standard verification benchmarks for bitvectors, and that it already complements the standard SMT approaches on several crucial (and industry-relevant) aspects, notably in terms of scalability w.r.t. bit-width, theory combination or intricate mix of non-linear arithmetic and bitwise operators. This work paves the way toward building competitive CP-based verification-oriented solvers.
Complete list of metadatas

Cited literature [47 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01795779
Contributor : Zakaria Chihani <>
Submitted on : Friday, May 18, 2018 - 4:58:27 PM
Last modification on : Thursday, February 7, 2019 - 3:26:44 PM
Long-term archiving on : Tuesday, September 25, 2018 - 6:32:56 PM

File

bv-cpaior.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01795779, version 1

Citation

Zakaria Chihani, Bruno Marre, François Bobot, Sébastien Bardin. Sharpening Constraint Programming approaches for Bit-Vector Theory. CPAIOR 2017. International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Jun 2017, Padova, Italy. ⟨cea-01795779⟩

Share

Metrics

Record views

86

Files downloads

121