Advertisement

A Generalization of Shostak#x2019;s Method for Combining Decision Procedures

  • Clark W. Barrett
  • David L. Dill
  • Aaron Stump
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2309)

Abstract

Consider the problem of determining whether a quantifier-free formula ϕ is satisfiable in some first-order theory T . Shostak#x2019;s algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak#x2019;s method. The first is a simple subset of Shostak's algorithm for the same class of theories but without uninterpreted function symbols. This simplified algorithm is easy to understand and prove correct, providing insight into how and why Shostak#x2019;s algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak's method based on a variation of the Nelson- Oppen method for combining theories.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    C. Barrett, D. Dill, and J. Levitt. Validity Checking for Combinations of Theories with Equality. In M. Srivas and A. Camilleri, eds., Formal Methods in Computer-Aided Design, volume 1166 of Lecture Notes in Computer Science, pages 187–201. Springer-Verlag, 1996.CrossRefGoogle Scholar
  2. 2.
    C. Barrett, D. Dill, and A. Stump. A Framework for Cooperating Decision Procedures. In 17th International Conference on Automated Deduction, Lecture Notes in Computer Science. Springer-Verlag, 2000.Google Scholar
  3. 3.
    Clark W. Barrett. Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories. PhD thesis, Stanford University, 2002.Google Scholar
  4. 4.
    Nikolaj S. Bjørner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University, 1999.Google Scholar
  5. 5.
    D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak’s Decision Procedure for Combinations of Theories. In M. McRobbie and J. Slaney, eds., 13th International Conference on Computer Aided Deduction, volume 1104 of Lecture Notes in Computer Science, pages 463–477. Springer-Verlag, 1996.Google Scholar
  6. 6.
    Z. Manna et al. STeP: Deductive-Algorithmic Verification of Reactive and Realtime Systems. In 8th International Conference on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 415–418. Springer-Verlag, 1996.Google Scholar
  7. 7.
    Jeremy R. Levitt. Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University, 1999.Google Scholar
  8. 8.
    G. Nelson and D. Oppen. Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–57, 1979.zbMATHCrossRefGoogle Scholar
  9. 9.
    Derek C. Oppen. Complexity, Convexity and Combinations of Theories. Theoretical Computer Science, 12:291–302, 1980.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    S. Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, ed., 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752. Springer-Verlag, 1992.Google Scholar
  11. 11.
    H. Ruess and N. Shankar. Deconstructing Shostak. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 19–28, June 2001.Google Scholar
  12. 12.
    Robert E. Shostak. Deciding Combinations of Theories. Journal of the Association for Computing Machinery, 31(1):1–12, 1984.zbMATHMathSciNetGoogle Scholar
  13. 13.
    C. Tinelli and M. Harandi. A New Correctness Proof of the Nelson-Oppen Combination Procedure. In F. Baader and K. Schulz, eds., 1st International Workshop on Frontiers of Combining Systems (FroCoS’96), volume 3 of Applied Logic Series. Kluwer Academic Publishers, 1996.Google Scholar
  14. 14.
    Ashish Tiwari. Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Clark W. Barrett
    • 1
  • David L. Dill
    • 1
  • Aaron Stump
    • 1
  1. 1.Stanford UniversityStanfordUSA

Personalised recommendations