Search papers, labs, and topics across Lattice.
This paper introduces Mosaic, a theory-modular framework that enhances the satisfiability decision process for Constrained Horn Clauses (CHCs) modulo fixed-size bit-vectors by integrating reasoning from both bit-vector and integer arithmetic theories. The motivation behind this work lies in the limitations of existing CHC solvers, which struggle with bit-precise reasoning, thereby hindering scalability in program verification. Experimental results demonstrate that Mosaic significantly outperforms the state-of-the-art Spacer solver on bit-manipulating benchmarks, showcasing its effectiveness in practical applications.
Mosaic's innovative modular reasoning approach enables substantial performance gains in bit-precise program verification, outperforming existing solvers.
Deciding satisfiability of Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors ($\mathcal{T}_B$) is fundamental to bit-precise program verification. However, state-of-the-art CHC-solvers often struggle with $\mathcal{T}_B$, limiting scalability in bit-precise reasoning. We present Mosaic, a theory-modular framework for deciding satisfiability of CHCs modulo $\mathcal{T}_B$ by combining reasoning in $\mathcal{T}_B$ and the theory of Integer Arithmetic ($\mathcal{T}_I$). Given a CHC set modulo $\mathcal{T}_B$, Mosaic partitions it into two fragments interpreted over $\mathcal{T}_B$ and $\mathcal{T}_I$. Moreover, it implements an algorithm that reasons about the fragments in a modular fashion, exchanges information between them via sound translations across theories, and determines satisfiability w.r.t. the original CHC set. We implemented a prototype of Mosaic using Z3 and Spacer and evaluated it on bit-manipulating benchmarks. Our evaluation shows that Mosaic significantly outperforms Spacer on these benchmarks.
