An Alternative to SAT-Based Approaches for Bit-Vectors

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 bitvector 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.

• Type: Conference
• Year: 2010
• Where: TACAS
• Authors: Sébastien Bardin, Philippe Herrmann, Florian Perroud
• Keywords: Algorithms, Resolution Techniques, SAT-based Resolution Techniques, Standard Low-level Machine, TACAS 2010