×

EufDPLL – a tool to check satisfiability of equality logic formulas. (English) Zbl 1336.68167

Seda, Anthony (ed.) et al., Proceedings of the Irish conference on the mathematical foundations of computer science and information technology (MFCSIT 2006), National University of Ireland, Cork, Ireland, August 1–5, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 225, 405-420 (2009).
Summary: Decision procedures for subsets of first-order logic form the core of many verification tools. Applications include hardware and software verification. The logic of Equality with Uninterpreted Functions (EUF) is a decidable subset of First-Order Logic. The EUF logic and its extensions have been applied for proving equivalence between systems. We present a branch and bound decision procedure for EUF logic based on the generalisation of the Davis-Putnam-Loveland-Logemann procedure (EUF-DPLL). EufDPLL is a tool to check satisfiability of EUF formulas based on this procedure.
For the entire collection see [Zbl 1279.68018].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
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] Badban, R.; de Pol, J.; Tveretina, O.; Zantema, H., Generalizing DPLL and Satisfiability for Equalities, Information and Computation, 205, 8, 1188-1211 (August 2007)
[3] Barrett, C. W.; Dill, D.; Levitt, J., Validity checking for combinations of theories with equality, (Srivas, M.; Camilleri, A., Formal Methods in Computer-Aided Design. Formal Methods in Computer-Aided Design, (FMCAD’96). Formal Methods in Computer-Aided Design. Formal Methods in Computer-Aided Design, (FMCAD’96), LNCS, vol. 1166 (November 1996), Springer-Verlag), 187-201
[4] Bryant, R.; Velev, M., Boolean satisfiability with transitivity constraints, ACM Transactions on Computational Logic, 3, 4, 604-627 (October 2002)
[5] Burch, J. R.; Dill, D. L., Automatic verification of pipelined microprocessor control, (Computer Aided Verification. Computer Aided Verification, Lecture Notes in Computer Science, Vol. 18 (1994), Springer-Verlag: Springer-Verlag Berlin)
[6] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Communications of the Association for Computing Machinery, 7, 394-397 (July 1962)
[7] Goel, A.; Sajid, K.; Zhou, H.; Aziz, A.; Singhal, V., BDD based procedures for a theory of equality with uninterpreted functions, (Hu, A. J.; Vardi, M. Y., Computer-Aided Verification. Computer-Aided Verification, (CAV’98). Computer-Aided Verification. Computer-Aided Verification, (CAV’98), LNCS, vol. 1427 (1998), Springer-Verlag), 244-255
[8] Groote, J.; van de Pol, J., Equational binary decision diagrams, (Parigot, M.; Voronkov, A., Logic for Programming and Reasoning. Logic for Programming and Reasoning, (LPAR’2000). Logic for Programming and Reasoning. Logic for Programming and Reasoning, (LPAR’2000), LNAI, vol. 1955 (2000)), 161-178 · Zbl 0988.68590
[9] Meir, O.; Strichman, O., Yet another decision procedure for equality logic proceedings, (17th International Conference on Computer Aided Verification. 17th International Conference on Computer Aided Verification, (CAV 2005). 17th International Conference on Computer Aided Verification. 17th International Conference on Computer Aided Verification, (CAV 2005), LNCS, vol. 3576 (2005)), 307-320 · Zbl 1081.68627
[10] Nieuwenhuis, R.; Oliveras, A., Congruence closure with integer offsets, (Vardi, M.; Voronkov, A., 10h Int. Conf. Logic for Programming, Artif. Intell. and Reasoning. 10h Int. Conf. Logic for Programming, Artif. Intell. and Reasoning, (LPAR). 10h Int. Conf. Logic for Programming, Artif. Intell. and Reasoning. 10h Int. Conf. Logic for Programming, Artif. Intell. and Reasoning, (LPAR), LNAI, 2850 (2003)), 78-90 · Zbl 1273.68326
[11] Nieuwenhuis, R.; Oliveras, A., Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools, (Proc. of 12th Int. Conf. Logic for Programming, Artificial Intelligecne and Reasoning. Proc. of 12th Int. Conf. Logic for Programming, Artificial Intelligecne and Reasoning, (LPAR). Proc. of 12th Int. Conf. Logic for Programming, Artificial Intelligecne and Reasoning. Proc. of 12th Int. Conf. Logic for Programming, Artificial Intelligecne and Reasoning, (LPAR), LNAI (2005)), 23-46 · Zbl 1143.68579
[12] Pnueli, A.; Rodeh, Y.; Shtrichman, O., Range allocation for equivalence logic, (Hariharan, R.; Mukund, M.; Vinay, V., Foundations of Software Technology and Theoretical Computer Science. Foundations of Software Technology and Theoretical Computer Science, (FSTTCS’01). Foundations of Software Technology and Theoretical Computer Science. Foundations of Software Technology and Theoretical Computer Science, (FSTTCS’01), LNCS, vol. 2245 (December 2001), Springer-Verlag), 317-333 · Zbl 1052.68088
[13] Pnueli, A.; Rodeh, Y.; Shtrichman, O.; Siegel, M., Deciding equality formulas by small domains instantiations, (Computer-Aided Verification. Computer-Aided Verification, (CAV’99). Computer-Aided Verification. Computer-Aided Verification, (CAV’99), LNCS (1999), Springer-Verlag) · Zbl 1046.68605
[14] Pnueli, A.; Rodeh, Y.; Shtrichman, O.; Siegel, M., The small model property: how small can it be?, Information and Computation, 178, 1, 279-293 (October 2002)
[15] Rodeh, Y.; Shtrichman, O., Finite instantiations in equivalence logic with uninterpreted functions, (Computer Aided Verification. Computer Aided Verification, (CAV’01). Computer Aided Verification. Computer Aided Verification, (CAV’01), LNCS, vol. 2102 (July 2001), Springer-Verlag), 144-154 · Zbl 0991.68045
[16] Shostak, R., An algorithm for reasoning about equality, Communications of the ACM, 21, 583-585 (July 1978)
[17] van den Brand, M. G.J.; de Jong, H. A.; Klint, P.; Olivier, P. A., Efficient Annotated Terms, Software, Practise and Experience, 30, 3, 259-291 (2000)
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.