×

Building small equality graphs for deciding equality logic with uninterpreted functions. (English) Zbl 1093.03013

Summary: The logic of equalities with uninterpreted functions is used in the formal verification community mainly for proofs of equivalence: proving that two versions of a hardware design are the same, or that input and output of a compiler are semantically equivalent are two prominent examples of such proofs. We introduce a new decision procedure for this logic that generalizes two leading decision procedures that were published in the last few years: the positive equality approach suggested by R. Bryant, S. German and M. Velev [“Exploiting positive equality in a logic of equality with uninterpreted functions”, Lect. Notes Comput. Sci. 1633, 470–482 (1999; Zbl 1046.68584)], and the range-allocation algorithm suggested by A. Pnueli, Y. Rodeh, O. Strichman and M. Siegel [“The small model property: how small can it be?” Inf. Comput. 178, 279–293 (2002; Zbl 1012.03040)]. Both of these methods reduce this logic to pure equality logic (without uninterpreted functions), and then, due to the small model property that such formulas have, find a small domain to each variable that is sufficiently large to maintain the satisfiability of the formula. The state-space spanned by these domains is then traversed with a BDD-based engine. The positive equality approach identifies terms that have a certain characteristic in the original formula (before the reduction to pure equality logic) and replaces them with unique constants. The range-allocation algorithm analyzes the structure of the formula after the reduction to equality logic with a graph-based procedure to allocate a small set of values to each variable. The former, therefore, has an advantage when a large subset of the terms can be replaced with constants, and disadvantage in the other cases. In this paper we essentially merge the two methods, while improving both with a more careful analysis of the formula’s structure. We show that the new method is provably dominant over both methods, theoretically as well as empirically.

MSC:

03B70 Logic in computer science
03B25 Decidability of theories and sets of sentences
12L05 Decidability and field theory
68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

ICS; EVC; CVC; UCLID; CVT
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ackermann, W., Solvable Cases of the Decision Problem, Studies in Logic and the Foundations of Mathematics (1954), North-Holland: North-Holland Amsterdam · Zbl 0056.24505
[2] G. Audemard, P. Bertoli, A. Cimatti, A. Kornilowicz, R. Sebastiani, A SAT based approach for solving formulas over boolean and linear mathematical propositions, in: Proc. 18th International Conference on Automated Deduction (CADE’02), 2002.; G. Audemard, P. Bertoli, A. Cimatti, A. Kornilowicz, R. Sebastiani, A SAT based approach for solving formulas over boolean and linear mathematical propositions, in: Proc. 18th International Conference on Automated Deduction (CADE’02), 2002. · Zbl 1072.68562
[3] R. Bryant, S. German, M. Velev, Exploiting positive equality in a logic of equality with uninterpreted functions, in: Proc. 11th Intl. Conference on Computer Aided Verification (CAV’99), 1999.; R. Bryant, S. German, M. Velev, Exploiting positive equality in a logic of equality with uninterpreted functions, in: Proc. 11th Intl. Conference on Computer Aided Verification (CAV’99), 1999. · Zbl 1046.68584
[4] Bryant, R.; German, S.; Velev, M., Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic, ACM Transactions on Computational Logic, 2, 1, 1-41 (2001) · Zbl 1365.68317
[5] Bryant, R.; Velev, M., Boolean satisfiability with transitivity constraints, (Emerson, E.; Sistla, A., Proc. 12th Intl. Conference on Computer Aided Verification (CAV’00). Proc. 12th Intl. Conference on Computer Aided Verification (CAV’00), Lecture Notes in Computer Science, vol. 1855 (2000), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0974.94501
[6] R. Bryant, M. Velev, Deciding a theory of positive equality with uninterpreted functions, Tech. Rep. CMU-CS-98-141, CMU (1998).; R. Bryant, M. Velev, Deciding a theory of positive equality with uninterpreted functions, Tech. Rep. CMU-CS-98-141, CMU (1998).
[7] Bryant, R.; Lahiri, S.; Seshia, S., Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions, (Brinksma, E.; Larsen, K., Proc. 14th Intl. Conference on Computer Aided Verification (CAV’02). Proc. 14th Intl. Conference on Computer Aided Verification (CAV’02), Lecture Notes in Computer Science, vol. 2404 (2002), Springer-Verlag: Springer-Verlag Copenhagen, Denmark), 78-91 · Zbl 1010.68522
[8] Bryant, R., Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers C-35, 12, 1035-1044 (1986)
[9] Burch, J. R.; Dill, D. L., Automatic verification of pipelined microprocessor control, (Proc. 6th Intl. Conference on Computer Aided Verification (CAV’94). Proc. 6th Intl. Conference on Computer Aided Verification (CAV’94), Lecture Notes in Computer Science, vol. 818 (1994), Springer-Verlag: Springer-Verlag Berlin), 68-80
[10] L. de Moura, H. Ruess, An experimental evaluation of ground decision procedures, in: R. Alur, D. Peled (Eds.), Proc. 16th Intl. Conference on Computer Aided Verification (CAV’03), Lect. Notes in Comp. Sci., Springer-Verlag, Boston, 2004.; L. de Moura, H. Ruess, An experimental evaluation of ground decision procedures, in: R. Alur, D. Peled (Eds.), Proc. 16th Intl. Conference on Computer Aided Verification (CAV’03), Lect. Notes in Comp. Sci., Springer-Verlag, Boston, 2004. · Zbl 1103.68645
[11] Filliatre, J.; Owre, S.; Rueb, H.; Shankar, N., ICS: integrated canonizer and solver, (Berry, G.; Comon, H.; Finkel, A., Proc. 13th Intl. Conference on Computer Aided Verification (CAV’01). Proc. 13th Intl. Conference on Computer Aided Verification (CAV’01), Lecture Notes in Computer Science (2001), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0996.68559
[12] Goel, A.; Sajid, K.; Zhou, H.; Aziz, A.; Singhal, V., BDD based procedures for a theory of equality with uninterpreted functions, (Hu, A.; Vardi, M., CAV98. CAV98, Lecture Notes in Computer Science, vol. 1427 (1998), Springer-Verlag: Springer-Verlag Berlin) · Zbl 1021.68057
[13] Lahiri, S.; Bryant, R.; Goel, A.; Talupur, M., Revisiting positive equality, (Tools and Algorithms for the Construction and Analysis of Systems TACAS 2004. Tools and Algorithms for the Construction and Analysis of Systems TACAS 2004, Lecture Notes in Computer Science, vol. 2988 (2004), Springer-Verlag: Springer-Verlag Berlin), 1-15 · Zbl 1126.68570
[14] S.K. Lahiri, S.A. Seshia, The UCLID decision procedure, in: R. Alur, D. Peled (Eds.), Proc. 16th Intl. Conference on Computer Aided Verification (CAV’03), Lect. Notes in Comp. Sci., Springer-Verlag, Boston, 2004.; S.K. Lahiri, S.A. Seshia, The UCLID decision procedure, in: R. Alur, D. Peled (Eds.), Proc. 16th Intl. Conference on Computer Aided Verification (CAV’03), Lect. Notes in Comp. Sci., Springer-Verlag, Boston, 2004. · Zbl 1103.68628
[15] Pnueli, A.; Rodeh, Y.; Strichman, O.; Siegel, M., The small model property: how small can it be?, Information and computation, 178, 1, 279-293 (2002) · Zbl 1012.03040
[16] Pnueli, A.; Siegel, M.; Shtrichman, O., The code validation tool (CVT)—automatic verification of a compilation process, International Journal of Software Tools for Technology Transfer (STTT), 2, 2, 192-201 (1999) · Zbl 1022.68733
[17] A. Pnueli, M. Siegel, O. Shtrichman, The code validation tool (CVT)—automatic verification of code generated from synchronous languages, in: B. Steffen (Ed.), Proc. of the Software Tools for Technology Transfer (STTT’98), 1998.; A. Pnueli, M. Siegel, O. Shtrichman, The code validation tool (CVT)—automatic verification of code generated from synchronous languages, in: B. Steffen (Ed.), Proc. of the Software Tools for Technology Transfer (STTT’98), 1998. · Zbl 1022.68733
[18] Pnueli, A.; Rodeh, Y.; Shtrichman, O.; Siegel, M., Deciding equality formulas by small-domains instantiations, (Proc. 11th Intl. Conference on Computer Aided Verification (CAV’99). Proc. 11th Intl. Conference on Computer Aided Verification (CAV’99), Lecture Notes in Computer Science (1999), Springer-Verlag: Springer-Verlag Berlin) · Zbl 1046.68605
[19] A. Pnueli, Y. Rodeh, O. Shtrichman, Range allocation for equivalence logic, in: Proc. 21st conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’01), Bangalore, India, 2001.; A. Pnueli, Y. Rodeh, O. Shtrichman, Range allocation for equivalence logic, in: Proc. 21st conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’01), Bangalore, India, 2001. · Zbl 1052.68088
[20] Rodeh, Y.; Shtrichman, O., Finite instantiations in equivalence logic with uninterpreted functions, (Berry, G.; Comon, H.; Finkel, A., Proc. 13th Intl. Conference on Computer Aided Verification (CAV’01). Proc. 13th Intl. Conference on Computer Aided Verification (CAV’01), Lecture Notes in Computer Science (2001), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0991.68045
[21] A. Stump, C. Barrett, D. Dill, CVC: a cooperating validity checker, in: Proc. 14th Intl. Conference on Computer Aided Verification (CAV’02), 2002.; A. Stump, C. Barrett, D. Dill, CVC: a cooperating validity checker, in: Proc. 14th Intl. Conference on Computer Aided Verification (CAV’02), 2002. · Zbl 1010.68720
[22] Velev, M.; Bryant, R., EVC: a validity checker for the logic of equality with uninterpreted functions and memories, exploiting positive equality, and conservative transformations, (Berry, G.; Comon, H.; Finkel, A., Proc. 13th Intl. Conference on Computer Aided Verification (CAV’01). Proc. 13th Intl. Conference on Computer Aided Verification (CAV’01), Lecture Notes in Computer Science, vol. 2102 (2001), Springer-Verlag: Springer-Verlag Berlin), 235-240 · Zbl 0996.68588
[23] M. Velev, Private communication.; M. Velev, Private communication.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.