Abstract
Stålmarck's 1-saturation algorithm is an incomplete but fast method for computing partial equivalence relations over propositional formulae. Aside from anecdotal evidence, until now little has been known about what it can prove. In this paper we characterize a set of formulae with bitvector- inequalities for which 1-saturation is sufficient to prove unsatisfiability. This result has application to fast predicate abstraction for software with fixed-width bit-vectors. © Springer-Verlag Berlin Heidelberg 2005.
Cite
CITATION STYLE
Cook, B., & Gonthier, G. (2005). Using Stålmarck’s algorithm to prove inequalities. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3785 LNCS, pp. 330–344). Springer Verlag. https://doi.org/10.1007/11576280_23
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
