The theory BV of bit-vectors, i.e. fixed-size arrays of bits equipped with standard low-level machine instructions, is becoming very popular in formal verification. Standard solvers for this theory are based on a bit-level encoding into propositional logic and SAT-based resolution techniques. In this paper, we investigate an alternative approach based on a word-level encoding into bounded arithmetic and Constraint Logic Programming (CLP) resolution techniques. We define an original CLP framework (domains and propagators) dedicated to bit-vector constraints. This framework is implemented in a prototype and thorough experimental studies have been conducted. The new approach is shown to perform much better than standard CLP-based approaches, and to considerably reduce the gap with the best SAT-based BV solvers. © 2010 Springer-Verlag.
CITATION STYLE
Bardin, S., Herrmann, P., & Perroud, F. (2010). An alternative to SAT-based approaches for bit-vectors. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6015 LNCS, pp. 84–98). https://doi.org/10.1007/978-3-642-12002-2_7
Mendeley helps you to discover research relevant for your work.