Name
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11576280_23 | ICFEM |
Keywords | Field | DocType |
partial equivalence relation,predicate abstraction,fast method,propositional formula,fixed-width bit-vectors,anecdotal evidence,1-saturation algorithm,equivalence relation | Discrete mathematics,Equivalence relation,Predicate abstraction,Abstract interpretation,Computer science,Algorithm,Software,Formal methods,Software development | Conference |
Volume | ISSN | ISBN |
3785 | 0302-9743 | 3-540-29797-9 |
Citations | PageRank | References |
2 | 0.38 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Byron Cook | 1 | 2 | 0.38 |
| Georges Gonthier | 2 | 2275 | 195.06 |