New results on rewrite-based satisfiability procedures

ABSTRACT

Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in theory T. If a sound and complete inference system for first-order logic is guaranteed to terminate on T-satisfiability problems, any theorem-proving strategy with that system and a fair search plan is a T-satisfiability procedure. We prove termination of a rewrite-based first-order engine on the theories of records, integer offsets, integer offsets modulo and lists. We give a modularity theorem stating sufficient conditions for termination on a combination of theories, given termination on each. The above theories, as well as others, satisfy these conditions. We introduce several sets of benchmarks on these theories and their combinations, including both parametric synthetic benchmarks to test scalability, and real-world problems to test performances on huge sets of literals. We compare the rewrite-based theorem prover E with the validity checkers CVC and CVC Lite. Contrary to the folklore that a general-purpose prover cannot compete with reasoners with built-in theories, the experiments are overall favorable to the theorem prover, showing that not only the rewriting approach is elegant and conceptually simple, but has important practical implications.

REFERENCES

• 1: Arkoudas, K., Zee, K., Kuncak, V., and Rinard, M. 2004. Verifying a file system implementation. In Proceedings of the 6th International Conference on Formal Engineering Methods. J. Davies, W. Schulte, and M. Barnett, Eds. Lecture Notes in Computer Science, vol. 3308. Springer-Verlag, Berlin, Germany, 373--390.
• 2: Armando, A., Bonacina, M. P., Ranise, S., Rusinowitch, M., and Sehgal, A. K. 2002. High-performance deduction for verification: A case study in the theory of arrays. In Notes 2nd VERIFY Workshop, FLoC. Tech. rep. 07/2002 DIKU, University of Copenhagen, Copenhagen, Denmark, 103--112.
• 3: Armando, A., Bonacina, M. P., Ranise, S., and Schulz, S. 2005a. Big proof engines as little proof engines: New results on rewrite-based satisfiability procedures. In Notes 3rd PDPAR Workshop, CAV-17. 33--41.
• 4: Armando, A., Bonacina, M. P., Ranise, S., and Schulz, S. 2005b. On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 65--80.
• 5: Alessandro Armando , Silvio Ranise , Michaël Rusinowitch, A rewriting approach to satisfiability procedures, Information and Computation, v.183 n.2, p.140-164, 15 June 2003 [doi>10.1016/S0890-5401(03)00020-8]
• 6: Baader, F. and Ghilardi, S. 2005. Connecting many-sorted structures and theories through adjoint functions. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 31--47.
• 7: Leo Bachmair , Ashish Tiwari , Laurent Vigneron, Abstract Congruence Closure, Journal of Automated Reasoning, v.31 n.2, p.129-168, 2003 [doi>10.1023/B:JARS.0000009518.26415.49]
• 8: Barrett, C. W. and Berezin, S. 2004. CVC lite: A new implementation of the cooperating validity checker. In Proceedings of the 16th International Conference on Computer-Aided Verification. R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 515--518.
• 9: Clark W. Barrett , David L. Dill , Aaron Stump, A Framework for Cooperating Decision Procedures, Proceedings of the 17th International Conference on Automated Deduction, p.79-98, June 17-20, 2000
• 10: Clark W. Barrett , David L. Dill , Aaron Stump, Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT, Proceedings of the 14th International Conference on Computer Aided Verification, p.236-249, July 27-31, 2002
• 11: Clark W. Barrett , David L. Dill , Aaron Stump, A Generalization of Shostak's Method for Combining Decision Procedures, Proceedings of the 4th International Workshop on Frontiers of Combining Systems, p.132-146, April 08-10, 2002
• 12: Bonacina, M. P. 1999. A taxonomy of theorem-proving strategies. In Artificial Intelligence Today—Recent Trends and Developments, M. J. Wooldridge and M. Veloso, Eds. Lecture Notes in Artificial Intelligence, vol. 1600. Springer-Verlag, Berlin, Germany, 43--84.
• 13: Maria Paola Bonacina , Nachum Dershowitz, Abstract canonical inference, ACM Transactions on Computational Logic (TOCL), v.8 n.1, p.6-es, January 2007 [doi>10.1145/1182613.1182619]
• 14: Maria Paola Bonacina , Mnacho Echenim, Rewrite-Based Decision Procedures, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.11, p.27-45, July, 2007 [doi>10.1016/j.entcs.2006.11.042]
• 15: Maria Paola Bonacina , Mnacho Echenim, Rewrite-Based Satisfiability Procedures for Recursive Data Structures, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.8, p.55-70, June, 2007 [doi>10.1016/j.entcs.2006.11.039]
• 16: Bonacina, M. P., Ghilardi, S., Nicolini, E., Ranise, S., and Zucchelli, D. 2006. Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In Proceedings of the IJCAR-3, U. Furbach and N. Shankar, Eds. Lecture Notes in Artificial Intelligence, vol. 4130. Springer-Verlag, Berlin, Germany, 513--527.
• 17: Maria Paola Bonacina , Jieh Hsiang, Towards a foundation of completion procedures as semidecision procedures, Theoretical Computer Science, v.146 n.1-2, p.199-242, July 24, 1995 [doi>10.1016/0304-3975(94)00187-N]
• 18: Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., Sebastiani, R., and van Rossum, P. 2005a. Efficient satisfiability modulo theories via delayed theory combination. In Proceedings of the 17th International Conference in Computer-Aided Verification, K. Etessami and S. Rajamani, Eds. Lecture Notes in Computer Science, vol. 3576. Springer-Verlag, Berlin, Germany, 335--349.
• 19: Marco Bozzano , Roberto Bruttomesso , Alessandro Cimatti , Tommi Junttila , Peter Rossum , Stephan Schulz , Roberto Sebastiani, MathSAT: Tight Integration of SAT and Mathematical Decision Procedures, Journal of Automated Reasoning, v.35 n.1-3, p.265-293, October 2005 [doi>10.1007/s10817-005-9004-z]
• 20: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 21: Randal E. Bryant , Steven German , Miroslav N. Velev, Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.93-134, Jan. 2001 [doi>10.1145/371282.371364]
• 22: Caferra, R., Leitsch, A., and Peltier, N. 2004. Automated Model Building. Kluwer Academic Publishers.
• 23: Chin-Liang Chang , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
• 24: Conchon, S. and Krstić, S. 2003. Strategies for combining decision procedures. In Proceedings of the International Conference on Tools and Algorithms for Constitution and Analysis of Systems, H. Garavel and J. Hatcliff, Eds. Lecture Notes in Computer Science, vol. 2619. Springer-Verlag, Berlin, Germany, 537--553.
• 25: David Cyrluk , Patrick Lincoln , Natarajan Shankar, On Shostak's Decision Procedure for Combinations of Theories, Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction, p.463-477, August 03, 1996
• 26: Cyrluk, D., Möller, O., and Ruess, H. 1996. An efficient decision procedure for a theory of fixed-sized bitvectors with composition and extraction. Tech. Rep. UIB96-08, Fakultät für Informatik, Universität Ulm, Ulm, Germany.
• 27: de Moura, L., Owre, S., Ruess, H., Rushby, J., and Shankar, N. 2004. The ICS decision procedures for embedded deduction. In Proceedings of the 2nd International Joint Conference on Automated Reasoning, D. Basin and M. Rusinowitch, Eds. Lecture Notes in Artificial Intelligence, vol. 3097. Springer-Verlag, Berlin, Germany, 218--222.
• 28: Leonardo M. de Moura , Harald Rueß , Maria Sorea, Lazy Theorem Proving for Bounded Model Checking over Infinite Domains, Proceedings of the 18th International Conference on Automated Deduction, p.438-455, July 27-30, 2002
• 29: Déharbe, D. and Ranise, S. 2003. Light-weight theorem proving for debugging and verifying units of code. In Proceedings SEFM03. IEEE Computer Society Press, Los Alamitos, CA.
• 30: Nachum Dershowitz, A Maximal-Literal Unit Strategy for Horn Clauses, Proceedings of the 2nd International CTRS Workshop on Conditional and Typed Rewriting Systems, p.14-25, June 11-14, 1990
• 31: Dershowitz, N. and Plaisted, D. A. 2001. Rewriting. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. 1. Elsevier, Amsterdam, The Netherlands, 535--610.
• 32: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 33: Peter Downey , Hanan Samet , Ravi Sethi, Off-line and on-line algorithms for deducing equalities, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.158-170, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512777]
• 34: Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
• 35: Dutertre, B. and de Moura, L. 2006. A fast linear-arithmetic solver for DPLL(T). In Proceedings of the International Conference on Computer-Aided Verification, T. Ball and R. B. Jones, Eds. Lecture Notes in Computer Science, vol. 4144. Springer-Verlag, Berlin, Germany, 81--94.
• 36: Christian G. Fermüller , Alexander Leitsch , Ullrich Hustadt , Tanel Tammet, Resolution decision procedures, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 37: Flanagan, C., Joshi, R., Ou, X., and Saxe, J. B. 2003. Theorem proving using lazy proof explication. In Proceedings of the International Conference on Computer-Aided Verification, J. Warren, W. A. Hunt, Jr., and F. Somenzi, Eds. Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, Berlin, Germany, 355--367.
• 38: Jean Gallier , Paliath Narendran , David Plaisted , Stan Raatz , Wayne Snyder, An algorithm for finding canonical sets of ground rewrite rules in polynomial time, Journal of the ACM (JACM), v.40 n.1, p.1-16, Jan. 1993 [doi>10.1145/138027.138032]
• 39: Harald Ganzinger, Shostak Light, Proceedings of the 18th International Conference on Automated Deduction, p.332-346, July 27-30, 2002
• 40: Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., and Tinelli, C. 2004a. DPLL(T): Fast decision procedures. In Proceedings of the 16th International Conference on Computer-Aided Verification (CAV'04), R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 175--188.
• 41: Ganzinger, H., Ruess, H., and Shankar, N. 2004b. Modularity and refinement in inference systems. Tech. Rep. CSL-SRI-04-02, SRI International, Menlo Park, CA.
• 42: Harald Ganzinger , Viorica Sofronie-Stokkermans , Uwe Waldmann, Modular proof systems for partial functions with Evans equality, Information and Computation, v.204 n.10, p.1453-1492, October 2006 [doi>10.1016/j.ic.2005.10.002]
• 43: Silvio Ghilardi, Model-Theoretic Methods in Combined Constraint Satisfiability, Journal of Automated Reasoning, v.33 n.3-4, p.221-249, October 2004 [doi>10.1007/s10817-004-6241-5]
• 44: Ghilardi, S., Nicolini, E., and Zucchelli, D. 2005. A comprehensive framework for combined decision procedures. In Proceedings of the 5th International Worshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 1--30.
• 45: Horn, A. 1951. On sentences which are true of direct unions of algebras. J. Symbol. Logic 16, 14--21.
• 46: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 47: Kaufmann, M., Manolios, P., and Moore, J. S. Eds. 2000. Computer Aided Reasoning: ACL2 Case Studies. Kluwer.
• 48: Kirchner, H., Ranise, S., Ringeissen, C., and Tran, D. K. 2005. On superposition-based satisfiability procedures and their combination. In Proceedings of 2nd ICTAC, D. Hung and M. Wirsing, Eds. Lecture Notes in Computer Science, vol. 3722. Springer-Verlag, Berlin, Germany, 594--608.
• 49: Knuth, D. E., and Bendix, P. B. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, J. Leech, Ed. Pergamon Press, Oxford, UK, 263--297.
• 50: Krstić, S. and Conchon, S. 2003. Canonization for disjoint unions of theories. In Proc. CADE-19, F. Baader, Ed. Lecture Notes in Computer Science, vol. 2741. Springer-Verlag, Berlin, Germany.
• 51: Lahiri, S. K. and Musuvathi, M. 2005a. An efficient decision procedure for UTVPI constraints. In Proceedings of the 5th FroCoS, B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 168--183.
• 52: Lahiri, S. K. and Musuvathi, M. 2005b. An efficient Nelson-Oppen decision procedure for difference constraints over rationals. In Notes 3rd PDPAR Workshop, CAV-17. 2--9.
• 53: Lahiri, S. K. and Seshia, S. A. 2004. The UCLID decision procedure. In Proceedings of CAV-16, R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 475--478.
• 54: Lankford, D. S. 1975. Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX.
• 55: Christopher Lynch , Barbara Morawska, Automatic Decidability, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.7, July 22-25, 2002
• 56: Christopher Lynch , Duc-Khanh Tran, Automatic Decidability and Combinability Revisited, Proceedings of the 21st international conference on Automated Deduction: Automated Deduction, July 17-20, 2007, Bremen, Germany [doi>10.1007/978-3-540-73595-3_22]
• 57: Manna, Z. and Zarba, C. G. 2003. Combining decision procedures. In Formal Methods at the Crossroads: From Panacea to Foundational Support. Lecture Notes in Computer Science, vol. 2757. Springer-Verlag, Berlin, Germany, 381--422.
• 58: McCune, W. W. 2003. Otter 3.3 reference manual. Tech. Rep. ANL/MCS-TM-263, MCS Division, Argonne National Laboratory, Argonne, IL, U.S.A.
• 59: Meir, O. and Strichman, O. 2005. Yet another decision procedure for equality logic. In Proceedings of the CAV-17, K. Etessami and S. Rajamani, Eds. Lecture Notes in Computer Science, vol. 3576. Springer-Verlag, Berlin, Germany, 307--320.
• 60: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 61: G. C. Necula , P. Lee, Efficient Representation and Validation of Proofs, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.93, June 21-24, 1998
• 62: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 63: Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
• 64: Robert Nieuwenhuis , Albert Oliveras, Fast congruence closure and extensions, Information and Computation, v.205 n.4, p.557-580, April, 2007 [doi>10.1016/j.ic.2006.08.009]
• 65: Nieuwenhuis, R. and Rubio, A. 2001. Paramodulation-based theorem proving. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. 1. Elsevier, Amsterdam, The Netherlands, 371--443.
• 66: Derek C. Oppen, Reasoning About Recursively Defined Data Structures, Journal of the ACM (JACM), v.27 n.3, p.403-411, July 1980 [doi>10.1145/322203.322204]
• 67: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 68: David A. Plaisted, Equational reasoning and term rewriting systems, Handbook of logic in artificial intelligence and logic programming (vol. 1), Oxford University Press, Inc., New York, NY, 1993
• 69: David A. Plaisted , Andrea Sattler-Klein, Proof lengths for equational completion, Information and Computation, v.125 n.2, p.154-170, March 15, 1996 [doi>10.1006/inco.1996.0028]
• 70: Ranise, S. and Déharbe, D. 2003. Light-weight theorem proving for debugging and verifying pointer manipulating programs. In Proceedings of FTP-2003, I. Dahn and L. Vigneron, Eds. Number DSCI--II710/03 in Technical Reports. Universidad Politécnica de Valencia, 119--132.
• 71: Ranise, S., Ringeissen, C., and Tran, D. K. 2004. Nelson-Oppen, Shostak and the extended canonizer: A family picture with a newborn. In Proceedings of the 1st ICTAC, K. Araki and Z. Liu, Eds. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany.
• 72: Ranise, S., Ringeissen, C., and Zarba, C. G. 2005. Combining data structures with nonstably infinite theories using many-sorted logic. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems. B. Gramlich, Ed. Lecture Notes in Artificial Intelligence, vol. 3717. Springer-Verlag, Berlin, Germany, 48--64.
• 73: Riazanov, A. and Voronkov, A. 2002. The design and implementation of VAMPIRE. J. AI Commun. 15, 2/3, 91--110.
• 74: Ruess, H. 2004. Personal communication on ICS 2.0 (e-mail message to Alessandro Armando).
• 75: Harald Rueβ , Natarajan Shankar, Deconstructing Shostak, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.19, June 16-19, 2001
• 76: Ruess, H. and Shankar, N. 2004. Solving linear arithmetic constraints. Tech. Rep. CSL-SRI-04-01, SRI International, Menlo Park, CA.
• 77: Schulz, S. 2002. E—A brainiac theorem prover. J. AI Commun. 15, 2--3, 111--126.
• 78: Schulz, S. 2004. System description: E 0.81. In Proceedings of the 2nd International Joint Conference on Automated Reasoning. D. Basin and M. Rusinowitch, Eds. Lecture Notes in Artificial Intelligence, vol. 3097. Springer-Verlag, Berlin, Germany, 2223--2228.
• 79: Schulz, S. and Bonacina, M. P. 2005. On handling distinct objects in the superposition calculus. In Notes 5th IWIL Workshop, LPAR-11. 66--77.
• 80: Sanjit A. Seshia , Shuvendu K. Lahiri , Randal E. Bryant, A hybrid SAT-based decision procedure for separation logic with uninterpreted functions, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775945]
• 81: Shankar, N. 2002. Little engines of proof. Invited talk, 3rd FLoC, Copenhagen, Denmark; and course notes of Fall 2003, http://www.csl.sri.com/users/shankar/LEP.html.
• 82: Robert E. Shostak, An algorithm for reasoning about equality, Communications of the ACM, v.21 n.7, p.583-585, July 1978 [doi>10.1145/359545.359570]
• 83: Robert E. Shostak, Deciding Combinations of Theories, Journal of the ACM (JACM), v.31 n.1, p.1-12, Jan. 1984 [doi>10.1145/2422.322411]
• 84: Stickel, M. E. 2002. Herbrand Award speech. 3rd FLoC, Copenhagen, Denmark.
• 85: Stump, A. 2005. Personal communication on CVC 1.0a (e-mail message to Alessandro Armando).
• 86: Aaron Stump , Clark W. Barrett , David L. Dill, CVC: A Cooperating Validity Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.500-504, July 27-31, 2002
• 87: Aaron Stump , Clark W. Barrett , David L. Dill , Jeremy Levitt, A Decision Procedure for an Extensional Theory of Arrays, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.29, June 16-19, 2001
• 88: Aaron Stump , David L. Dill, Faster Proof Checking in the Edinburgh Logical Framework, Proceedings of the 18th International Conference on Automated Deduction, p.392-407, July 27-30, 2002
• 89: Tinelli, C. and Harandi, M. 1996. A new correctness proof of the Nelson-Oppen combination procedure. In Proceedings of the 1st FroCoS, F. Baader and K. Schulz, Eds. Applied Logic Series, vol. 3. Kluwer Academic Publishers.
• 90: van Dalen, D. 1989. Logic and Structure. Springer-Verlag, Berlin, Germany. Second edition.
• 91: Christoph Weidenbach, System Description: Spass Version 1.0.0, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.378-382, July 07-10, 1999

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Inference engines

General Terms:
Performance, Theory, Verification

Keywords:
Automated reasoning, combination of theories, decision procedures, inference, rewriting, satisfiability modulo a theory, scalability, superposition, termination