[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Little Engines of Proof

  • Conference paper
  • First Online:
FME 2002:Formal Methods—Getting IT Right (FME 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2391))

Included in the following conference series:

Abstract

The automated construction of mathematical proof is a basic activity in computing. Since the dawn of the field of automated reasoning, there have been two divergent schools of thought. One school, best represented by Alan Robinson’s resolution method, is based on simple uniform proof search procedures guided by heuristics. The other school, pioneered by Hao Wang, argues for problem-specific combinations of decision and semi-decision procedures. While the former school has been dominant in the past, the latter approach has greater promise. In recent years, several high quality inference engines have been developed, including propositional satisfiability solvers, ground decision procedures for equality and arithmetic, quantifier elimination procedures for integers and reals, and abstraction methods for finitely approximating problems over infinite domains. We describe some of these “little engines of proof” and a few of the ways in which they can be combined. We focus in particular on combining different decision procedures for use in automated verification.

Funded by NSF Grants CCR-0082560 and CCR-9712383, DARPA/AFRL Contract F33615-00-C-3043, and NASA Contract NAS1-20334. John Rushby, Sam Owre, Ashish Tiwari, and Tomás Uribe commented on earlier drafts of this paper.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 71.50
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 89.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, May 1993.

    Google Scholar 

  2. R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3–34, 6 February 1995.

    Google Scholar 

  3. Kai Baukus, Saddek Bensalem, Yassine Lakhnech, and Karsten Stahl. Abstracting WS1S systems to verify parameterized networks. In Susanne Graf and Michael Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), number 1785 in Lecture Notes in Computer Science, pages 188–203, Berlin, Germany, March 2000. Springer-Verlag.

    Chapter  Google Scholar 

  4. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.

    Google Scholar 

  5. Clark W. Barrett, David L. Dill, and Aaron Stump. A framework for cooperating decision procedures. In David McAllester, editor, Automated Deduction—CADE-17, volume 1831 of Lecture Notes in Artificial Intelligence, pages 79–98, Pittsburgh, PA, June 2000. Springer-Verlag.

    Google Scholar 

  6. Clark W. Barrett, David L. Dill, and Aaron Stump. Checking satisfiability of first-order formulas by incremental translation to SAT. In Computer-Aided Verification, CAV’ 02, Lecture Notes in Computer Science. Springer-Verlag, July 2002.

    Google Scholar 

  7. Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001 [RV01]}, pages 19–99.

    Google Scholar 

  8. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.

    Google Scholar 

  9. Nikolaj Bjørner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University, 1999.

    Google Scholar 

  10. W. W. Bledsoe. Non-resolution theorem proving. Artificial Intelligence, 9:1–36, 1977.

    Article  MATH  MathSciNet  Google Scholar 

  11. Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 319–331.

    Chapter  Google Scholar 

  12. Saddek Bensalem, Yassine Lakhnech, and Sam Owre. InVeSt: A tool for the verification of invariants. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 505–510.

    Chapter  Google Scholar 

  13. R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, New York, NY, 1979.

    MATH  Google Scholar 

  14. R. S. Boyer and J S. Moore. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In R. S. Boyer and J S. Moore, editors, The Correctness Problem in Computer Science. Academic Press, London, 1981.

    Google Scholar 

  15. R. S. Boyer and J S. Moore. Integrating decision procedures into heuristic theorem provers: A case study with linear arithmetic. In Machine Intelligence, volume 11. Oxford University Press, 1986.

    Google Scholar 

  16. T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of the SIGPLAN’ 01 Conference on Programming Language Design and Implementation, 2001, pages 203–313. ACM Press, 2001.

    Google Scholar 

  17. R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.

    Google Scholar 

  18. Alexander Bockmayr and Volker Weispfenning. Solving numerical constraints. In A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001 [RV01]}, pages 751–742.

    Google Scholar 

  19. James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering, pages 439–448, Limerick, Ireland, June 2000. IEEE Computer Society.

    Google Scholar 

  20. Shang-Ching Chou and Xiao-Shan Gao. Automated reasoning in geometry. In A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001 [RV01]}, pages 707–749.

    Google Scholar 

  21. E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Nineteenth Annual ACM Symposium on Principles of Programming Languages, pages 343–354, 1992.

    Google Scholar 

  22. E. M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999.

    Google Scholar 

  23. G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition. Journal of Symbolic Computation, 12(3):299–328, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  24. G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Second GI Conference on Automata Theory and Formal Languages, number 33 in Lecture Notes in Computer Science, pages 134–183, Berlin, 1975. Springer-Verlag.

    Google Scholar 

  25. D. C. Cooper. Theorem proving in arithmetic without multiplication. In Machine Intelligence 7, pages 91–99. Edinburgh University Press, 1972.

    MATH  Google Scholar 

  26. M. A. Colón and T. E. Uribe. Generating finite-state abstractions of reactive systems using decidion procedures. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 293–304.

    Chapter  Google Scholar 

  27. M. Davis. A computer program for Presburger’s algorithm. In Summaries of Talks Presented at the Summer Institute for Symbolic Logic, 1957. Reprinted in Siekmann and Wrightson [SW83], pages 41–48.

    Google Scholar 

  28. M. Davis. The prehistory and early history of automated deduction. In G. Wrightson, editors. Automation of Reasoning: Classical Papers on Computational Logic, Volumes 1 & 2. Springer-Verlag, 1983 [SW83]}, pages 1–28.

    Google Scholar 

  29. Satyaki Das and David L. Dill. Successive approximation of abstract transition relations. In Annual IEEE Symposium on Logic in Computer Science01, pages 51–60. The Institute of Electrical and Electronics Engineers, 2001.

    Google Scholar 

  30. Satyaki Das, David L. Dill, and Seungjoon Park. Experience with predicate abstraction. In Nicolas Halbwachs and Doron Peled, editors, Computer-Aided Verification, CAV’ 99, volume 1633 of Lecture Notes in Computer Science, pages 160–171, Trento, Italy, July 1999. Springer-Verlag.

    Chapter  Google Scholar 

  31. George B. Dantzig and B. Curtis Eaves. Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory (A), 14:288–297, 1973.

    Article  MATH  MathSciNet  Google Scholar 

  32. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394–397, July 1962. Reprinted in Siekmann and Wrightson [SW83], pages 267–270, 1983.

    Google Scholar 

  33. David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Technical Report 159, COMPAQ Systems Research Center, 1998.

    Google Scholar 

  34. Leonardo de Moura, Harald Rueß, and Maria Sorea. Lazy theorem proving for bounded model checking over infinite domains. In A. Voronkov, editor, International Conference on Automated Deduction (CADE’02), Lecture Notes in Computer Science, Copenhagen, Denmark, July 2002. Springer-Verlag.

    Google Scholar 

  35. M. Davis and H. Putnam. A computing procedure for quantification theory. JACM, 7(3):201–215, 1960.

    Article  MATH  MathSciNet  Google Scholar 

  36. Jacob Elgaard, Nils Klarlund, and Anders Möller. Mona 1.x: New techniques for WS1S and WS2S. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 516–520.

    Chapter  Google Scholar 

  37. J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar. ICS: Integrated Canonization and Solving. In G. Berry, H. Comon, and A. Finkel, editors, Computer-Aided Verification, CAV’ 2001, volume 2102 of Lecture Notes in Computer Science, pages 246–249, Paris, France, July 2001. Springer-Verlag.

    Google Scholar 

  38. Cormac Flanagan and Shaz Qadeer. Predicate abstraction for software verification. In ACM Symposium on Principles of Programming Languages02, pages 191–202. Association for Computing Machinery, January 2002.

    Google Scholar 

  39. Jonathan Ford and Natarajan Shankar. Formal verification of a combination decision procedure. In A. Voronkov, editor, Proceedings of CADE-19, Berlin, Germany, 2002. Springer-Verlag.

    Google Scholar 

  40. P. C. Gilmore. A proof method for quantification theory: Its justification and realization. IBM Journal of Research and Development, 4:28–35, 1960. Reprinted in Siekmann and Wrightson [SW83], pages 151–161, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  41. M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

    MATH  Google Scholar 

  42. Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella, and Moshe Y. Vardi. Towards an efficient library for SAT: a manifesto. To appear, 2002.

    Google Scholar 

  43. S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In Conference on Computer Aided Verification CAV’97, LNCS 1254, Springer Verlag, 1997.

    Google Scholar 

  44. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Lazy abstraction. In ACM Symposium on Principles of Programming Languages02, pages 58–70. Association for Computing Machinery, January 2002.

    Google Scholar 

  45. G. Huet and D. C. Oppen. Equations and rewrite rules: a survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349–405. Academic Press, ny, 1980.

    Google Scholar 

  46. Alan J. Hu and Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag.

    Google Scholar 

  47. Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Computer-Aided Reasoning: An Approach, volume 3 of Advances in Formal Methods. Kluwer, 2000.

    Google Scholar 

  48. R.P. Kurshan. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1993.

    Google Scholar 

  49. C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:11–44, 1995.

    Article  MATH  Google Scholar 

  50. D. C. Luckham, S. M. German, F. W. von Henke, R. A. Karp, P. W. Milne, D. C. Oppen, W. Polak, and W. L. Scherlis. Stanford Pascal Verifier user manual. CSD Report STAN-CS-79-731, Stanford University, Stanford, CA, March 1979.

    Google Scholar 

  51. K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, 1993.

    MATH  Google Scholar 

  52. Marvin Minsky. Steps toward artificial intelligence. In E. A. Feigenbaum and J. Feldman, editors, Computers and Thought. McGraw-Hill Book Company, New York, 1963.

    Google Scholar 

  53. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Design Automation Conference, pages 530–535, 2001.

    Google Scholar 

  54. J. Marques-Silva and K. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506–521, May 1999.

    Google Scholar 

  55. Zohar Manna and The STeP Group. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV’ 96, volume 1102 of Lecture Notes in Computer Science, pages 415–418, New Brunswick, NJ, July/August 1996. Springer-Verlag.

    Google Scholar 

  56. George C. Necula. Proof-carrying code. In 24th ACM Symposium on Principles of Programming Languages, pages 106–119, Paris, France, January 1997. Association for Computing Machinery.

    Google Scholar 

  57. G. Nelson. Techniques for program verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center, Palo Alto, Ca., 1981.

    Google Scholar 

  58. G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, 1979.

    Article  MATH  Google Scholar 

  59. A. Newell, J. C. Shaw, and H. A. Simon. Empirical explorations with the logic theory machine: A case study in heuristics. In Proc. West. Joint Comp. Conf., pages 218–239, 1957. Reprinted in Siekmann and Wrightson [SW83], pages 49–73, 1983.

    Google Scholar 

  60. Derek C. Oppen. A \( 2^{2^{2^{pn} } } \) upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences, 16:323–332, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  61. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer-Verlag.

    Google Scholar 

  62. Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.

    Google Scholar 

  63. E. L. Post. Introduction to a general theory of elementary propositions. American Journal of Mathematics, 43:163–185, 1921. Reprinted in [vH67, pages 264–283].

    Article  MathSciNet  MATH  Google Scholar 

  64. D. Prawitz. An improved proof procedure. Theoria, 26:102–139, 1960. Reprinted in Siekmann and Wrightson [SW83], pages 162–201, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  65. M. Presburger. Uber die vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. Compte Rendus du congrés Mathématiciens des Pays Slaves, pages 92–101, 1929.

    Google Scholar 

  66. W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102–114, 1992.

    Article  Google Scholar 

  67. Michael O. Rabin. Decidable theories. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter C8, pages 595–629. North-Holland, Amsterdam, Holland, 1978.

    Google Scholar 

  68. J. A. Robinson. A machine-oriented logic based on the resolution principle. JACM, 12(1):23–41, 1965. Reprinted in Siekmann and Wright-son [SW83], pages 397–415.

    Article  MATH  Google Scholar 

  69. Harald Rueß and Natarajan Shankar. Deconstructing Shostak. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 19–28, Boston, MA, July 2001. IEEE Computer Society.

    Google Scholar 

  70. A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001.

    Google Scholar 

  71. Natarajan Shankar. Using decision procedures with a higher-order logic. In Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science, pages 5–26, Edinburgh, Scotland, September 2001. Springer-Verlag. Available at ftp://ftp.csl.sri.com/pub/users/shankar/tphols2001.ps.gz.

    Chapter  Google Scholar 

  72. Robert E. Shostak. Deciding linear inequalities by computing loop residues. Journal of the ACM, 28(4):769–779, October 1981.

    Google Scholar 

  73. Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1–12, January 1984.

    Google Scholar 

  74. T. R. Shiple, J. H. Kukula, and R. K. Ranjan. A comparison of Presburger engines for EFSM reachability. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 280–292.

    Chapter  Google Scholar 

  75. Natarajan Shankar and Sam Owre. Principles and pragmatics of subtyping in PVS. In D. Bert, C. Choppy, and P. D. Mosses, editors, Recent Trends in Algebraic Development Techniques, WADT’ 99, volume 1827 of Lecture Notes in Computer Science, pages 37–52, Toulouse, France, September 1999. Springer-Verlag.

    Google Scholar 

  76. N. Shankar and H. Rueß. Combining Shostak theories. In International Conference on Rewriting Techniques and Applications (RTA’ 02), Lecture Notes in Computer Science. Springer-Verlag, July 2002. Invited Paper.

    Google Scholar 

  77. Hassen Saïdi and Natarajan Shankar. Abstract and model check while you prove. In Computer-Aided Verification, CAV’ 99, Trento, Italy, July 1999.

    Google Scholar 

  78. Mary Sheeran and Gunnar Stålmarck. A tutorial on Stålmarck’s proof procedure for propositional logic. Formal Methods in Systems Design, 16(1):23–58, January 2000.

    Google Scholar 

  79. R. E. Shostak, R. Schwartz, and P. M. Melliar-Smith. STP: A mechanized logic for specification and verification. In D. Loveland, editor, 6th International Conference on Automated Deduction (CADE), volume 138 of Lecture Notes in Computer Science, New York, NY, 1982. Springer-Verlag.

    Google Scholar 

  80. J. Siekmann and G. Wrightson, editors. Automation of Reasoning: Classical Papers on Computational Logic, Volumes 1 & 2. Springer-Verlag, 1983.

    Google Scholar 

  81. A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, 1948.

    Google Scholar 

  82. Cesare Tinelli and Mehdi Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In Frans Baader and Klaus U. Schulz, editors, Frontiers of Combining Systems: First International Workshop, volume 3 of Applied Logic Series, pages 103–119, Munich, Germany, March 1996. Kluwer.

    Google Scholar 

  83. Laurent Théry. A certified version of Buchberger’s algorithm. In H. Kirchner and C. Kirchner, editors, Proceedings of CADE-15, number 1421 in Lecture Notes in Artificial Intelligence, pages 349–364, Berlin, Germany, July 1998. Springer-Verlag.

    Google Scholar 

  84. Ashish Tiwari. Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook, 2000.

    Google Scholar 

  85. Ashish Tiwari and Gaurav Khanna. Series of abstractions for hybrid automata. In C.J. Tomlin and M.R. Greenstreet, editors, Hybrid Systems: Computation and Control, 5th International Workshop, HSCC 2002, volume 2289 of Lecture Notes in Computer Science, pages 465–478, Stanford, CA, March 2002. Springer-Verlag.

    Chapter  Google Scholar 

  86. J. van Heijenoort, editor. From Frege to Gödel: A Sourcebook of Mathematical Logic, 1879-1931. Harvard University Press, Cambridge, MA, 1967.

    Google Scholar 

  87. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings 1st Annual IEEE Symp. on Logic in Computer Science, pages 332–344. IEEE Computer Society Press, 1986.

    Google Scholar 

  88. H. Wang. Proving theorems by pattern recognition — I. Communications of the ACM, 3(4):220–234, 1960. Reprinted in Siekmann and Wrightson [SW83], pages 229–243, 1983.

    Article  MATH  Google Scholar 

  89. Hao Wang. Toward mechanical mathematics. IBM Journal, 4:2–22, 1960.

    MATH  Google Scholar 

  90. H. Wang. Mechanical mathematics and inferential analysis. In P. Braffort and D. Hershberg, editors, Computer Programming and Formal Systems. North-Holland, 1963.

    Google Scholar 

  91. Richard W. Weyhrauch. Prolegomena to a theory of mechanized formal reasoning. Artificial Intelligence, 13(1 and 2):133–170, April 1980.

    Google Scholar 

  92. Hantao Zhang. SATO: An efficient propositional prover. In Conference on Automated Deduction, pages 272–275, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Laboratory, SRI International, Menlo Park, CA, 94025, USA

    Natarajan Shankar

Authors
  1. Natarajan Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Information Technology, Uppsala University, P.O. Box 337, 751 05, Uppsala, Sweden

    Lars-Henrik Eriksson

  2. Software Verification Research Centre, The University of Queensland, Queensland, 4072, Australia

    Peter Alexander Lindsay

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Shankar, N. (2002). Little Engines of Proof. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-45614-7_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43928-8

  • Online ISBN: 978-3-540-45614-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation