Abstract

We characterize a set of formulas with bitvector inequalities for which Stalmark’s 1-saturation algorithm is complete. This result has applications to fast predicate abstraction for software with fixed-width bitvectors.

‚Äč