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.
Supplemental Material
Available for Download
Benchmarks for the experiments conducted in Simplify: a theorem prover for program checking
Online appendix to designing mediation for context-aware applications. The appendix supports the information on page 365.
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- Chvatal, V. 1983. Linear Programming. W H Freeman & Co.Google Scholar
- 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 Scholar
- Crocker, S. 1988. Comparison of Shostak's and Oppen's solvers. Unpublished manuscript.Google Scholar
- Dantzig, G. B. 1963. Linear Programming and Extensions. Princeton University Press, Princeton, NJ.Google Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- Downey, P. J., Sethi, R., and Tarjan, R. E. 1980. Variations on the common subexpression problem. JACM 27, 4 (Oct.), 758--771. Google Scholar
- 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 Scholar
- 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 Scholar
- Galler, B. A., and Fischer, M. J. 1964. An improved equivalence algorithm. CACM 7, 5, 301--303. Google Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- Knuth, D. E. 1968. The Art of Computer Programming---Vol. 1 Fundamental Algorithms. Addison Wesley, Reading, MA. 2nd ed. 1973. Google Scholar
- 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 Scholar
- Kozen, D. 1977. Complexity of finitely presented algebras. In Proceedings Ninth STOC. 164--177. Google Scholar
- 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 Scholar
- 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 Scholar
- Loveland, D. W. 1978. Automated Theorem Proving: A Logical Basis. Elsevier Science. Google Scholar
- Marcus, L. 1981. A comparison of two simplifiers. Microver Note 94, SRI. January.Google Scholar
- Marriott, K., and Stuckey, P. J. 1998. Programming with Constraints: An Introduction. MIT Press, Cambridge, MA.Google Scholar
- McCarthy, J. 1963. Towards a mathematical science of computation. In Information Processing: The 1962 IFIP Congress. 21--28.Google Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- 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 Scholar
- Nelson, G. 1981. Techniques for program verification. Technical Report CSL-81-10, Xerox PARC Computer Science Laboratory. June.Google Scholar
- 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 Scholar
- 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 Scholar
- Nelson, G., and Oppen, D. C. 1980. Fast decision procedures based on congruence closure. JACM 27, 2 (April), 356--364. Google Scholar
- 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 Scholar
- Rabin, M. O. 1981. Fingerprinting by random polynomials. Technical Report TR-15-81, Center for Research in Computing Technology, Harvard University.Google Scholar
- Ruess, H., and Shankar, N. 2001. Deconstructing Shostak. In Proceedings of the LICS 2001. 10--28. Google Scholar
- Schmitt, P. H. 2003. Personal communication (email message to Greg Nelson).Google Scholar
- Shankar, N. 2003. Personal communication (email message to James B. Saxe).Google Scholar
- 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 Scholar
- Shostak, R. E. 1979. A practical decision procedure for arithmetic with function symbols. JACM 26, 2 (April), 351--360. Google Scholar
- Shostak, R. E. 1984. Deciding combinations of theories. JACM 31, 1, 1--12. See also {Barrett et al. 2002b; Ruess and Shankar 2001}. Google Scholar
- 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 Scholar
- 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 Scholar
- Stuckey, P. J. 1991. Incremental linear constraint solving and detection of implicit equalities. ORSA Journal on Computing 3, 4, 269--274.Google Scholar
- 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 Scholar
- Tarjan, R. E. 1975. Efficiency of a good but not linear set union algorithm. JACM 22, 2, 215--225. Google Scholar
- 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 Scholar
- Yao, A. 1976. On the average behavior of set merging algorithms. In 8th ACM Symposium on the Theory of Computation. 192--195. Google Scholar
- Zhang, H. 1997. SATO: An efficient propositional prover. In Proceedings of the 14th International Conference on Automated Deduction. 272--275. Google Scholar
Index Terms
Simplify: a theorem prover for program checking
Recommendations
On Deciding Satisfiability by Theorem Proving with Speculative Inferences
Applications in software verification often require determining the satisfiability of first-order formulae with respect to background theories. During development, conjectures are usually false. Therefore, it is desirable to have a theorem prover that ...
Verified heap theorem prover by paramodulation
ICFP '12We present VeriStar, a verified theorem prover for a decidable subset of separation logic. Together with VeriSmall [3], a proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully machine-checked static analyses ...
DT-an automated theorem prover for multiple-valued first-order predicate logics
ISMVL '96: Proceedings of the 26th International Symposium on Multiple-Valued LogicWe describe the automated theorem prover "Deep Thought" (DT). The prover can be used for arbitrary multiple-valued first-order logics, provided the connectives can be defined by truth tables and the quantifiers are generalizations of the classical ...
Comments