Name
Abstract | ||
|---|---|---|
In a CAV'05 paper [Meir, O. and O. Strichman, Yet another decision procedure for equality logic, in: K. Etessami and S. Rajamani, editors, Proc. 17^t^h Intl. Conference on Computer Aided Verification (CAV'05), Lect. Notes in Comp. Sci. 3576 (2005), pp. 307-320] we introduced a new decision procedure for Equality Logic: each equality predicate is encoded with a Boolean variable, and then a set of transitivity constraints are added to compensate for the loss of transitivity of equality. The constraints are derived by analyzing Contradictory Cycles: cycles in the equality graph with exactly one disequality. Such a cycle is called constrained under a formula @f if @f is not satisfied with an assignment of true to all equality edges and false to the disequality edge. While we proved in [Meir, O. and O. Strichman, Yet another decision procedure for equality logic, in: K. Etessami and S. Rajamani, editors, Proc. 17^t^h Intl. Conference on Computer Aided Verification (CAV'05), Lect. Notes in Comp. Sci. 3576 (2005), pp. 307-320] that it is sufficient to constrain all simple contradictory cycles, we left open the question of how to find the necessary constraints in polynomial time. Instead, we showed two possible compromises: an exponential algorithm, or, alternatively, a polynomial approximation that constrains all contradictory cycles rather than only the simple ones. In this article we show a polynomial algorithm that constrains only the simple contradictory cycles. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1016/j.entcs.2008.04.077 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
generating minimum transitivity constraints,decision procedure,contradictory cycle,equality graph,h intl,k. etessami,simple contradictory cycle,equality logic,s. rajamani,equalities with uninterpreted functions,equality predicate,equality edge,polynomial time | Graph,Discrete mathematics,Exponential function,Polynomial,Polynomial algorithm,Predicate (grammar),Boolean data type,Time complexity,Mathematics,Transitive relation | Journal |
Volume | Issue | ISSN |
198 | 2 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
1 | 0.35 | 4 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mirron Rozanov | 1 | 1 | 0.35 |
| Ofer Strichman | 2 | 1071 | 63.61 |