Equational Bit-Vector Solving via Strong Gröbner Bases
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要