An alternative to SAT-based approaches for bit-vectors. (English) Zbl 1284.68379

Bardin, Sébastien; Herrmann, Philippe; Perroud, Florian

Esparza, Javier (ed.) et al., Tools and algorithms for the construction and analysis of systems. 16th international conference, TACAS 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-12001-5/pbk). Lecture Notes in Computer Science 6015, 84-98 (2010).

Summary: 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.
For the entire collection see [Zbl 1185.68007].

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
03B05	Classical propositional logic
68N17	Logic programming
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Beaver; GATeL; MathSAT; Prolog