Equational Bit-Vector Solving via Strong Gröbner Bases

Jiaxin Song, Hongfei Fu, Charles Zhang

Bit-vectors, which are integers in a finite number of bits, are ubiquitous in software and hardware systems. In this work, we consider the satisfiability modulo theories (SMT) of b…