Bit-Precise CHC Satisfiability Using Theory-Modular Reasoning

Omer Rappoport, Orna Grumberg, Yakir Vizel

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…