George Rennie

Sound and Complete Solving for Multi-width Parametric Bitvectors via Principled Reductions

Bitvectors are foundational for automated reasoning about programs, and fixed-width bitvector solvers (QF_BV) are fast and ubiquitous. However, the theory of parametric bitvectors (PBV), where widths are symbolic, is much less well understood. The theory of multi-width PBV, where...