skip to main content
article

Simplify: a theorem prover for program checking

Published:01 May 2005Publication History
Skip Abstract Section

Abstract

This article provides a detailed description of the automatic theorem prover Simplify, which is the proof engine of the Extended Static Checkers ESC/Java and ESC/Modula-3. Simplify uses the Nelson--Oppen method to combine decision procedures for several important theories, and also employs a matcher to reason about quantifiers. Instead of conventional matching in a term DAG, Simplify matches up to equivalence in an E-graph, which detects many relevant pattern instances that would be missed by the conventional approach. The article describes two techniques, error context reporting and error localization, for helping the user to determine the reason that a false conjecture is false. The article includes detailed performance figures on conjectures derived from realistic program-checking problems.

Skip Supplemental Material Section

Supplemental Material

References

  1. Agesen, O., Detlefs, D. L., Flood, C. H., Garthwaite, A. T., Martin, P. A., Shavit, N. N., and Steel, Jr., G. L. 2000. Dcas-based concurrent deques. In ACM Symposium on Parallel Algorithms and Architectures. 137--146. Google ScholarGoogle Scholar
  2. Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., and Schmitt, P. H. 2003. The KeY tool. Technical report in computing science no. 2003--5, Department of Computing Science, Chalmers University and Göteborg University, Göteborg, Sweden. February.Google ScholarGoogle Scholar
  3. Badros, G. J., Borning, A., and Stuckey, P. J. 2001. The Cassowary linear arithmetic constraint solving algorithm. ACM Transactions on Computer-Human Interaction 8, 4 (Dec.), 267--306. Google ScholarGoogle Scholar
  4. Ball, T., Majumdar, R., Millstein, T. D., and Rajamani, S. K. 2001. Automatic predicate abstraction of C programs. In SIGPLAN Conference on Programming Language Design and Implementation. Snowbird, Utah. 203--213. Google ScholarGoogle Scholar
  5. Barrett, C. W. 2002. Checking validity of quantifier-free formulas in combinations of first-order theories. Ph.D. thesis, Department of Computer Science, Stanford University, Stanford, CA. Available at http://verify.stanford.edu/barrett/thesis.ps.Google ScholarGoogle Scholar
  6. Barrett, C. W., Dill, D. L., and Levitt, J. 1996. Validity checking for combinations of theories with equality. In Proceedings of Formal Methods In Computer-Aided Design. 187--201. Google ScholarGoogle Scholar
  7. Barrett, C. W., Dill, D. L., and Levitt, J. R. 1998. A decision procedure for bit-vector arithmetic. In Proceedings of the 35th Design Automation Conference. San Francisco, CA. Google ScholarGoogle Scholar
  8. Barrett, C. W., Dill, D. L., and Stump, A. 2002a. Checking satisfiability of first-order formulas by incremental translation to SAT. In Proceedings of the 14th International Conference on Computer-Aided Verification, E. Brinksma and K. G. Larsen, Eds. Number 2404 in Lecture Notes in Computer Science. Springer-Verlag. Copenhagen. Google ScholarGoogle Scholar
  9. Barrett, C. W., Dill, D. L., and Stump, A. 2002b. A generalization of Shostak's method for combining decision procedures. In Frontiers of Combining Systems (FROCOS). Lecture Notes in Artificial Intelligence. Springer-Verlag. Santa Margherita di Ligure, Italy. Google ScholarGoogle Scholar
  10. Bibel, W., and Eder, E. 1993. Methods and calculi for deduction. In Handbook of Logic in Artificial Intelligence and Logic Programming---Vol 1: Logical Foundations., D. M. Gabbay, C. J. Hogger, and J. A. Robinson, Eds. Clarendon Press, Oxford, 67--182. Google ScholarGoogle Scholar
  11. Chvatal, V. 1983. Linear Programming. W H Freeman & Co.Google ScholarGoogle Scholar
  12. Conchon, S., and Krstić, S. 2003. Strategies for combining decision procedures. In Proceedings of the 9th International Conferences on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03). Lecture Notes in Computer Science, vol. 2619. Springer Verlag, 537--553. Google ScholarGoogle Scholar
  13. Crocker, S. 1988. Comparison of Shostak's and Oppen's solvers. Unpublished manuscript.Google ScholarGoogle Scholar
  14. Dantzig, G. B. 1963. Linear Programming and Extensions. Princeton University Press, Princeton, NJ.Google ScholarGoogle Scholar
  15. de Moura, L., and Ruess, H. 2002. Lemmas on demand for satisfiability solvers. In Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing.Google ScholarGoogle Scholar
  16. de Moura, L. M., and Ruess, H. 2004. An experimental evaluation of ground decision procedures. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV), R. Alur and D. A. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer, 162--174. See http://www.csl.sri.com/users/demoura/gdp-benchmarks.html for benchmarks and additional results.Google ScholarGoogle Scholar
  17. Detlefs, D., and Moir, M. 2000. Mechanical proofs of correctness for dcas-based concurrent deques. Available at http://research.sun.com/jtech/pubs/00-deque1-proof.html.Google ScholarGoogle Scholar
  18. Detlefs, D., Nelson, G., and Saxe, J. B. 2003a. Simplify benchmarks. Available at http://www. hpl.hp.com/research/src/esc/simplify_benchmarks.tar.gz. These benchmarks are also available in the appendix to the online version of this article, available via the ACM Digital Library.Google ScholarGoogle Scholar
  19. Detlefs, D., Nelson, G., and Saxe, J. B. 2003b. Simplify source code. Available at http://www. research.compaq.com/downloads.html as part of the Java Programming Toolkit Source Release.Google ScholarGoogle Scholar
  20. Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. 1998. Extended static checking. Research Report 159, Compaq Systems Research Center, Palo Alto, USA. December. Available at http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-159.html.Google ScholarGoogle Scholar
  21. Downey, P. J., Sethi, R., and Tarjan, R. E. 1980. Variations on the common subexpression problem. JACM 27, 4 (Oct.), 758--771. Google ScholarGoogle Scholar
  22. Flanagan, C., Joshi, R., Ou, X., and Saxe, J. B. 2003. Theorem proving using lazy proof explication. In Proceedings of the 15th International Conference on Computer Aided Verification. 355--367.Google ScholarGoogle Scholar
  23. Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for java. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming language Design and Implementation (PLDI'02). Berlin, 234--245. Google ScholarGoogle Scholar
  24. Galler, B. A., and Fischer, M. J. 1964. An improved equivalence algorithm. CACM 7, 5, 301--303. Google ScholarGoogle Scholar
  25. Ganzinger, H. 2002. Shostak light. In Proceedings 18th International Conference on Automated Deduction (CADE 18), A. Voronkov, Ed. Lecture Notes in Computer Science, vol. 2392. Springer, Copenhagen, 332--346. Google ScholarGoogle Scholar
  26. Ganzinger, H., Ruess, H., and Shankar, N. 2004. Modularity and refinement in inference systems. CSL Technical Report CSL-SRI-04-02, SRI. Dec. Available at ftp://ftp.csl.sri.com/pub/users/shankar/modularity.ps.gz.Google ScholarGoogle Scholar
  27. Guerra e Silva, L., Marques-Silva, J., and Silveira, L. M. 1999. Algorithms for solving boolean satisfiability in combinational circuits. In Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE). Munich, 526--530. Google ScholarGoogle Scholar
  28. Gulwani, S., and Necula, G. C. 2003. A randomized satisfiability procedure for arithmetic and uninterpreted function symbols. In 19th International Conference on Automated Deduction. LNCS, vol. 2741. Springer-Verlag, 167--181.Google ScholarGoogle Scholar
  29. Joshi, R., Nelson, G., and Randall, K. 2002. Denali: A goal-directed superoptimizer. In Proceedings of the ACM 2002 Conference on Programming Language Design and Implementation. Berlin, 304--314. Google ScholarGoogle Scholar
  30. Knuth, D. E. 1968. The Art of Computer Programming---Vol. 1 Fundamental Algorithms. Addison Wesley, Reading, MA. 2nd ed. 1973. Google ScholarGoogle Scholar
  31. Knuth, D. E., and Schönhage, A. 1978. The expected linearity of a simple equivalence algorithm. Theoretical Computer Science 6, 3 (June), 281--315.Google ScholarGoogle Scholar
  32. Kozen, D. 1977. Complexity of finitely presented algebras. In Proceedings Ninth STOC. 164--177. Google ScholarGoogle Scholar
  33. Krstić, S., and Conchon, S. 2003. Canonization for disjoint unions of theories. In Proceedings of the 19th International Conference on Automated Deduction (CADE-19), F. Baader, Ed. Lecture Notes in Computer Science, vol. 2741. Springer Verlag.Google ScholarGoogle Scholar
  34. Liskov, B., Atkinson, R., Bloom, T., Moss, J. E. B., Schaffert, C., Scheifler, R., and Snyder, A. 1981. CLU Reference Manual. Lecture Notes in Computer Science, vol. 114. Springer-Verlag, Berlin. Google ScholarGoogle Scholar
  35. Loveland, D. W. 1978. Automated Theorem Proving: A Logical Basis. Elsevier Science. Google ScholarGoogle Scholar
  36. Marcus, L. 1981. A comparison of two simplifiers. Microver Note 94, SRI. January.Google ScholarGoogle Scholar
  37. Marriott, K., and Stuckey, P. J. 1998. Programming with Constraints: An Introduction. MIT Press, Cambridge, MA.Google ScholarGoogle Scholar
  38. McCarthy, J. 1963. Towards a mathematical science of computation. In Information Processing: The 1962 IFIP Congress. 21--28.Google ScholarGoogle Scholar
  39. Millstein, T. 1999. Toward more informative ESC/Java warning messages. In Compaq SRC Technical Note 1999-003. Available at http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1999-003.html.Google ScholarGoogle Scholar
  40. Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., and Malik, S. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the 39th Design Automation Conference. Google ScholarGoogle Scholar
  41. Necula, G. C. 1998. Compiling with Proofs. Ph.D. thesis, Carnegie-Mellon University. Also available as CMU Computer Science Technical Report CMU-CS-98-154. Google ScholarGoogle Scholar
  42. Necula, G. C., and Lee, P. 2000. Proof generation in the Touchstone theorem prover. In Proceedings of the 17th International Conference on Automated Deduction. 25--44. Google ScholarGoogle Scholar
  43. Nelson, C. G. 1979. Techniques for program verification. Ph.D. thesis, Stanford University. A revised version of this thesis was published as a Xerox PARC Computer Science Laboratory Research Report {Nelson 1981}. Google ScholarGoogle Scholar
  44. Nelson, G. 1981. Techniques for program verification. Technical Report CSL-81-10, Xerox PARC Computer Science Laboratory. June.Google ScholarGoogle Scholar
  45. Nelson, G. 1983. Combining satisfiability procedures by equality-sharing. In Automatic Theorem Proving: After 25 Years, W. W. Bledsoe and D. W. Loveland, Eds. American Mathematical Society, 201--211.Google ScholarGoogle Scholar
  46. Nelson, G., and Oppen, D. C. 1979. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1, 2 (Oct.), 245--257. Google ScholarGoogle Scholar
  47. Nelson, G., and Oppen, D. C. 1980. Fast decision procedures based on congruence closure. JACM 27, 2 (April), 356--364. Google ScholarGoogle Scholar
  48. Owre, S., Rushby, J. M., and Shankar, N. 1992. PVS: A prototype verification system. In 11th International Conference on Automated Deduction (CADE), D. Kapur, Ed. Lecture Notes in Artificial Intelligence, vol. 607. Springer-Verlag, Saratoga, NY, 748--752. Available at http://www.csl.sri.com/papers/cade92-pvs/. Google ScholarGoogle Scholar
  49. Rabin, M. O. 1981. Fingerprinting by random polynomials. Technical Report TR-15-81, Center for Research in Computing Technology, Harvard University.Google ScholarGoogle Scholar
  50. Ruess, H., and Shankar, N. 2001. Deconstructing Shostak. In Proceedings of the LICS 2001. 10--28. Google ScholarGoogle Scholar
  51. Schmitt, P. H. 2003. Personal communication (email message to Greg Nelson).Google ScholarGoogle Scholar
  52. Shankar, N. 2003. Personal communication (email message to James B. Saxe).Google ScholarGoogle Scholar
  53. Shankar, N., and Ruess, H. 2002. Combining Shostak theories. Invited paper for Floc'02/RTA'02. Available at ftp://ftp.csl.sri.com/pub/users/shankar/rta02.ps. Google ScholarGoogle Scholar
  54. Shostak, R. E. 1979. A practical decision procedure for arithmetic with function symbols. JACM 26, 2 (April), 351--360. Google ScholarGoogle Scholar
  55. Shostak, R. E. 1984. Deciding combinations of theories. JACM 31, 1, 1--12. See also {Barrett et al. 2002b; Ruess and Shankar 2001}. Google ScholarGoogle Scholar
  56. Silva, J. M., and Sakallah, K. A. 1999. GRASP: A search algorithm for propositionsal satisfiability. IEEE Transactions on Computers 48, 5 (May), 506--521. Google ScholarGoogle Scholar
  57. Stallman, R. M., and Sussman, G. J. 1977. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence 9, 2 (Oct.), 135--196.Google ScholarGoogle Scholar
  58. Stuckey, P. J. 1991. Incremental linear constraint solving and detection of implicit equalities. ORSA Journal on Computing 3, 4, 269--274.Google ScholarGoogle Scholar
  59. Stump, A., Barrett, C., Dill, D., and Levitt, J. 2001. A decision procedure for an extensional theory of arrays. In 16th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 29--37. Google ScholarGoogle Scholar
  60. Tarjan, R. E. 1975. Efficiency of a good but not linear set union algorithm. JACM 22, 2, 215--225. Google ScholarGoogle Scholar
  61. Tinelli, C., and Harandi, M. T. 1996. A new correctness proof of the Nelson-Oppen combination procedure. In Frontiers of Combining Systems: Proceedings of the 1st International Workshop, F. Baader and K. U. Schulz, Eds. Kluwer Academic Publishers, Munich, 103--120.Google ScholarGoogle Scholar
  62. Yao, A. 1976. On the average behavior of set merging algorithms. In 8th ACM Symposium on the Theory of Computation. 192--195. Google ScholarGoogle Scholar
  63. Zhang, H. 1997. SATO: An efficient propositional prover. In Proceedings of the 14th International Conference on Automated Deduction. 272--275. Google ScholarGoogle Scholar

Index Terms

  1. Simplify: a theorem prover for program checking

                Recommendations

                Reviews

                Dachuan Yu

                Automated theorem proving has attracted much attention, notably in the fields of integrated circuit design and software verification. Simplify is an automated theorem prover for first-order formulas. Although it is a research prototype, Simplify has been used as a proof engine in some well-known projects, including extended static checking (ESC), the SLAM Static Driver Verifier, and the Spec# programming system. This paper provides a thorough description of Simplify, which is based on a combination of both mature research results in the field and novel techniques designed for the specific goal of program checking. Given an arbitrary first-order formula with quantification, it is not always possible to recognize its validity with automatic theorem proving. Nonetheless, in the context of program checking, the goal of Simplify is to find simple proofs rapidly when they exist. Since the queries to Simplify are typically verification conditions for the absence of specific programming errors, rather than general formulas, it appears that the incompleteness is not as essential as the sufficient level of automation and performance. Simplify handles quantifiers with a matcher that heuristically chooses relevant instances, reducing the query to quantifier-free formulas, which are in turn reasoned with a backtracking search for finding satisfying assignments. This paper documents the key aspects of Simplify, including the combined decision procedures for the theories of equality and linear rational arithmetic, the built-in theories for maps and partial orders, the heuristics for linear integer arithmetic for improving performance, and the pattern-driven instantiation of quantified formulas. It provides both high-level descriptions with examples and detailed algorithms for carrying out the ideas efficiently. It also describes techniques for helping the user determine the reason for an error. Furthermore, it includes performance figures for evaluating the practicality of the techniques and the effectiveness of the heuristics. Although recent advances in decision procedures have surpassed it on unquantified formulas, Simplify seems to be a good choice for quantified formulas. More importantly, this paper serves as a thorough documentation of Simplify for a wide range of audiences. It is self-contained, so an informed outsider with a background in logic can easily pick up the basics. It also documents efficient implementation details, design alternatives, and potential improvements. Therefore, it is helpful for beginners learning automatic theorem proving, people using Simplify as part of other software, and researchers exploring related solutions. Online Computing Reviews Service

                Access critical reviews of Computing literature here

                Become a reviewer for Computing Reviews.

                Comments

                Login options

                Check if you have access through your login credentials or your institution to get full access on this article.

                Sign in

                Full Access

                PDF Format

                View or Download as a PDF file.

                PDF

                eReader

                View online with eReader.

                eReader