Using Stalmark’s Algorithm to Prove Inequalities

Byron Cook; Georges Gonthier

Using Stalmark’s Algorithm to Prove Inequalities

Byron Cook ,
Georges Gonthier

November 2005

Published by Springer-Verlag

Download BibTex

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.