Linear Arithmetic with Bit-Vectors using Omega and SAT
Daniel Kröning · Repository for Publications and Research Data (ETH Zurich) · 2005
Formal analysis tools for system-level software rely on solving de cision problems over bit-vector arithmetic. The common approach to decide these problems is to transform the constraints into a corresponding circuit at the net-list level, and then transform this net-list into CNF. The CNF is passed to a modern SAT-solver. The word-level structure of the original problem is lost. The Omega test is a decision procedure for a conjunction of linear constraints over integers. It is used for variable dependency analysis within compilers. In the hardware domain, a linearization of bit-vector operators has been applied successfully to data-paths. This paper proposes a variant of such an encoding to solve bit-vector arithmetic decision problems arising in software verification. A SAT solver is used for the case-splitting. We present preliminary experimental results comparing the new algorithm with the commonly used approach men tioned above.