Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Equational Bit-Vector Solving via Strong Gröbner Bases

Jiaxin Song, Hongfei Fu, Charles Zhang

TL;DR

This work tackles SMT for fixed-size bit-vectors by exploiting the algebraic structure of BV arithmetic through strong Gröbner bases over the ring $\mathbb{Z}_{2^d}$. It presents a quantifier-free solver for the equational BV theory, an algorithmic improvement for computing multiplicative inverses modulo a power of two, and a method for generating polynomial loop invariants via invariant templates and linear congruence solving. A complete invariant-generation workflow is provided, including a parametric normal form and a backtracking procedure to ensure completeness. Experimental results on extensive benchmarks show improved time efficiency and memory usage over state-of-the-art solvers, with notable gains in unsatisfiable instances and polynomial invariant generation performance. Overall, the paper demonstrates that incorporating strong Gröbner bases yields tangible performance benefits for BV SMT and loop-invariant synthesis, suggesting promising directions for broader BV arithmetics and integration with synthesis tasks.

Abstract

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 bit-vectors. Unlike normal integers, the arithmetics of bit-vectors are modular upon integer overflow. Therefore, the SMT solving of bit-vectors needs to resolve the underlying modular arithmetics. In the literature, two prominent approaches for SMT solving are bit-blasting (that transforms the SMT problem into boolean satisfiability) and integer solving (that transforms the SMT problem into integer properties). Both approaches ignore the algebraic properties of the modular arithmetics and hence could not utilize these properties to improve the efficiency of SMT solving. In this work, we consider the equational theory of bit-vectors and capture the algebraic properties behind them via strong Gröbner bases. First, we apply strong Gröbner bases to the quantifier-free equational theory of bit-vectors and propose a novel algorithmic improvement in the key computation of multiplicative inverse modulo a power of two. Second, we resolve the important case of invariant generation in quantified equational bit-vector properties via strong Gröbner bases and linear congruence solving. Experimental results over an extensive range of benchmarks show that our approach outperforms existing methods in both time efficiency and memory consumption.

Equational Bit-Vector Solving via Strong Gröbner Bases

TL;DR

This work tackles SMT for fixed-size bit-vectors by exploiting the algebraic structure of BV arithmetic through strong Gröbner bases over the ring . It presents a quantifier-free solver for the equational BV theory, an algorithmic improvement for computing multiplicative inverses modulo a power of two, and a method for generating polynomial loop invariants via invariant templates and linear congruence solving. A complete invariant-generation workflow is provided, including a parametric normal form and a backtracking procedure to ensure completeness. Experimental results on extensive benchmarks show improved time efficiency and memory usage over state-of-the-art solvers, with notable gains in unsatisfiable instances and polynomial invariant generation performance. Overall, the paper demonstrates that incorporating strong Gröbner bases yields tangible performance benefits for BV SMT and loop-invariant synthesis, suggesting promising directions for broader BV arithmetics and integration with synthesis tasks.

Abstract

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 bit-vectors. Unlike normal integers, the arithmetics of bit-vectors are modular upon integer overflow. Therefore, the SMT solving of bit-vectors needs to resolve the underlying modular arithmetics. In the literature, two prominent approaches for SMT solving are bit-blasting (that transforms the SMT problem into boolean satisfiability) and integer solving (that transforms the SMT problem into integer properties). Both approaches ignore the algebraic properties of the modular arithmetics and hence could not utilize these properties to improve the efficiency of SMT solving. In this work, we consider the equational theory of bit-vectors and capture the algebraic properties behind them via strong Gröbner bases. First, we apply strong Gröbner bases to the quantifier-free equational theory of bit-vectors and propose a novel algorithmic improvement in the key computation of multiplicative inverse modulo a power of two. Second, we resolve the important case of invariant generation in quantified equational bit-vector properties via strong Gröbner bases and linear congruence solving. Experimental results over an extensive range of benchmarks show that our approach outperforms existing methods in both time efficiency and memory consumption.
Paper Structure (28 sections, 13 theorems, 19 equations, 2 figures, 4 tables, 4 algorithms)

This paper contains 28 sections, 13 theorems, 19 equations, 2 figures, 4 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Rings, Polynomials and the Ring of Bit-Vectors
  4. Strong Gröbner Bases
  5. Quantifier-Free Equational Bit-Vector Theory
  6. SMT Solving with Strong Gröbner Bases
  7. Algorithmic Improvement for Multiplicative Inverse
  8. Loop Invariant Generation
  9. Inductive Loop Invariants
  10. Polynomial Invariants Generation over Bit-Vectors
  11. Implementation and Experimental Results
  12. Implementation
  13. Quantifier-Free Equational Bit-Vector Theory
  14. Polynomial Invariant Generation
  15. Related Works
  16. ...and 13 more sections

Key Result

Theorem 4

When $R$ is a PIR and $F\subseteq R[\bm{x}]$ is finite, Algorithm 6.4 of norton2001strong always returns a strong Gröbner basis of $\left\langle F\right\rangle$ in finite time.

Figures (2)

  • Figure : Finding the multiplicative inverse of $a$ over $\mathbb{Z}_{2^d}$ when $a$ is small.
  • Figure :

Theorems & Definitions (31)

  • Definition 1: Principal Ideal Ring greuel2008singular
  • Definition 2: Strong Reduction
  • Definition 3: Strong Gröbner Basis norton2001strong
  • Theorem 4
  • Proposition 5
  • Proposition 6
  • Proposition 7
  • Theorem 8
  • proof
  • Definition 9: S-polynomials norton2001strong
  • ...and 21 more