Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Using Stalmark's Algorithm to Prove Inequalities

Byron Cook and Georges Gonthier

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.

Details

Publication typeInproceedings
URLhttp://www.springer-ny.com/
PublisherSpringer-Verlag
> Publications > Using Stalmark's Algorithm to Prove Inequalities