Finite Instantiations in Equivalence Logic with Uninterpreted Functions

Yoav Rodeh Ofer Shtrichman

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

We introduce a decision procedure for satisfiability of equivalence logic formulas with uninterpreted functions and predicates. In a previous work, we presented a decision procedure for this problem which starts by reducing the formula into a formula in equality logic. As a second step, the formula structure was analyzed in order to derive a small range of values for each variable that is sufficient for preserving the formula's satisfiability. Then, a standard BDD based tool was used in order to check the formula under the new small domain. In this paper we change the reduction method and perform a more careful analysis of the formula, which results in significantly smaller domains. Both theoretical and experimental results show that the new method is superior to the previous one and to other methods that were suggested in the last few years.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems