Date: Tue, 31 Mar 92 20:19:44 CST From: Robert S. Boyer To: clt@sail.stanford.edu Below is a two year old list of applications of Nqthm and Pc-Nqthm, and some pointers to relevant or related (sometimes very vaguely related) documents. This is from a CADE-10 paper by Boyer and Moore. We and others have used NQTHM to check the correctness of many small programs. However, after many years of effort, we are beginning to see mechanical correctness proofs of entire small computing systems. By far, the most significant application of NQTHM has been to a prove the correctness of a computing system known as the CLI Stack, which includes (a) a microprocessor design (FM8502) based on gates and registers [38], (b) an assembler (Piton) [61] that targets FM8502, and (c) a higher level language (micro Gypsy) [76] that targets Piton. We have also seen a proof of correctness of a small operating system kernel (KIT) [2]. Except for the Piton work, all of these projects represent Ph.D. dissertations in computer science which we supervised at the University of Texas. FM8502, Piton, micro Gypsy, and Kit are documented in one place, a special issue of the Journal of Automated Reasoning [62]. Another major application of NQTHM is the Ph.D. work of N. Shankar in proof checking Godel's incompleteness theorem [69]. The text of this proof effort is included in the standard distribution of NQTHM, along with Shankar's checking of the Church-Rosser theorem. On pp. 4-9 of ACLH, we enumerate many other applications of NQTHM, including those in list processing, elementary number theory, metamathematics, set theory, and concurrent algorithms. Descriptions of some of these applications may be found in [16, 66, 12, 21, 17, 67, 68, 69, 20, 60, 28, 51, 37, 52, 13, 1 in [1, 31, 32, 33, 40, 75, 3, 48, 44, 41, 42, 39, 45, 23, 24, 25] Recently colleagues of ours at Computational Logic, Inc., Bill Young and Bill Bevier, have used NQTHM to construct mechanically checked proofs of properties relating to fault-tolerance. A key problem facing the designers of systems which attempt to ensure fault tolerance by redundant processing is how to guarantee that the processors reach agreement, even when one or more processing units are faulty. This problem, called the Byzantine Generals problem or the problem of achieving interactive consistency, was posed and solved by Pease, Shostak, and Lamport [64, 50]. They proved that the problem is solvable if and only if the total number of processors exceeds three times the number of faulty processors and devised an extremely clever algorithm (the ``Oral Messages'' Algorithm) which implements a solution to this problem. Bill Young and Bill Bevier, have just finished developing a machine checked proof of the correctness of this algorithm using NQTHM. Matt Kaufmann, of Computational Logic, Inc., has made extensive additions to NQTHM, building a system called ``PC-NQTHM'' on top of NQTHM, which many find more convenient than NQTHM for checking proofs. Information about PC-NQTHM and some extensions and applications may be found in [46, 49, 45, 47, 63, 43, 76]. Among the theorems which Kaufmann has checked with PC-NQTHM are: - Ramsey's theorem for exponent 2 (both finite and infinite versions), with explicit bound in the finite case [41, 46]. - Correctness of an algorithm of Gries for finding the largest ``true square'' submatrix of a boolean matrix [40]. - The Cantor-Schroeder-Bernstein theorem [46]. - The correctness of a Towers of Hanoi program. - The irrationality of the square root of 2. - Correctness of a finite version of the collapsing function of Cohen forcing. REFERENCES 1. W. Bevier. A Verified Operating System Kernel. Ph.D. Th., University of Texas at Austin, 1987. 2. W. R. Bevier. "Kit and the Short Stack". Journal of Automated Reasoning 5, 4 (1989), 519-530. 3. William Bevier, Matt Kaufmann, and William Young. Translation of a Gypsy Compiler Example into the Boyer-Moore Logic. Internal Note 169, Computational Logic, Inc., January, 1990. 4. W.W. Bledsoe. "Splitting and Reduction Heuristics in Automatic Theorem Proving". Artificial Intelligence 2 (1971), 55-77. 5. W. Bledsoe, R. Boyer, and W. Henneman. "Computer Proofs of Limit Theorems". Artificial Intelligence 3 (1972), 27-60. 6. N. Bourbaki. Elements of Mathematics. Addison Wesley, Reading, Massachusetts, 1968. 7. R. S. Boyer and J S. Moore. "Program Verification". Journal of Automated Reasoning 1, 1 (1985), 17-23. 8. R. S. Boyer, D. M. Goldschlag, M. Kaufmann, and J S. Moore. Functional Instantiation in First Order Logic, Report 44. Computational Logic, 1717 W. 6th St., Austin, Texas, 78703, U.S.A., 1989. To appear in the proceedings of the 1989 Workshop on Programming Logic, Programming Methodology Group, University of Goteborg. 9. R. S. Boyer and J S. Moore. "Proving Theorems about LISP Functions". JACM 22, 1 (1975), 129-144. 10. R. S. Boyer and J S. Moore. A Lemma Driven Automatic Theorem Prover for Recursive Function Theory. Proceedings of the 5th Joint Conference on Artificial Intelligence, 1977, pp. 511-519. 11. R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, New York, 1979. 12. R. S. Boyer and J S. Moore. Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures. In The Correctness Problem in Computer Science, R. S. Boyer and J S. Moore, Eds., Academic Press, London, 1981. 13. R. S. Boyer and J S. Moore. A Verification Condition Generator for FORTRAN. In The Correctness Problem in Computer Science, R. S. Boyer and J S. Moore, Eds., Academic Press, London, 1981. 14. R. S. Boyer and J S. Moore. The Mechanical Verification of a FORTRAN Square Root Program. SRI International, 1981. 15. R. S. Boyer and J S. Moore. MJRTY - A Fast Majority Vote Algorithm. Technical Report ICSCA-CMP-32, Institute for Computing Science and Computer Applications, University of Texas at Austin, 1982. 16. R. S. Boyer and J S. Moore. "Proof Checking the RSA Public Key Encryption Algorithm". American Mathematical Monthly 91, 3 (1984), 181-189. 17. R. S. Boyer and J S. Moore. "A Mechanical Proof of the Unsolvability of the Halting Problem". JACM 31, 3 (1984), 441-458. 18. R. S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, New York, 1988. 19. R. S. Boyer and J S. Moore. Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study with Linear Arithmetic. In Machine Intelligence 11, Oxford University Press, 1988. 20. R. S. Boyer and J S. Moore. "The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover". Journal of Automated Reasoning 4 (1988), 117-172. 21. R. S. Boyer and J S. Moore. A Mechanical Proof of the Turing Completeness of Pure Lisp. In Automated Theorem Proving: After 25 Years, W.W. Bledsoe and D.W. Loveland, Eds., American Mathematical Society, Providence, R.I., 1984, pp. 133-167. 22. R. S. Boyer, M. W. Green and J S. Moore. The Use of a Formal Simulator to Verify a Simple Real Time Control Program. In Beauty Is Our Business, Springer, 1990, pp. 55-64. 23. A. Bronstein and C. Talcott. String-Functional Semantics for Formal Verification of Synchronous Circuits, Report No. STAN-CS-88-1210. Computer Science Department, Stanford University, 1988. 24. A. Bronstein. MLP: String-functional semantics and Boyer-Moore mechanization for the formal verification of synchronous circuits. Ph.D. Th., Stanford University, 1989. 25. A. Bronstein and C. Talcott. Formal Verification of Synchronous Circuits based on String-Functional Semantics: The 7 Paillet Circuits in Boyer-Moore. C-Cube 1989 Workshop on Automatic Verification Methods for Finite State Systems. LNCS 407, 1989, pp. 317-333. 26. R. Burstall. "Proving Properties of Programs by Structural Induction". The Computer Journal 12, 1 (1969), 41-48. 27. S. Chou. Mechancial Geometry Theorem Proving. Reidel, 1988. 28. Benedetto Lorenzo Di Vito. Verification of Communications Protocols and Abstract Process Models. Ph.D. Th., University of Texas at Austin, 1982. 29. T. L. Heath (translation and commentary). The Thirteen Books of Euclid's Elements. Dover, New York , 1908. p. 298, Vol 2., i.e. Proposition 2, Book VII. 30. R. Floyd. Assigning Meanings to Programs. In Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, American Mathematical Society, Providence, Rhode Island, 1967, pp. 19-32. 31. David M. Goldschlag. "Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover". IEEE Transactions on Software Engineering (September 1990). To appear. 32. David M. Goldschlag. Mechanizing Unity. In Proceedings of the IFIP TC2/WG2.3 Working Conference on Programming Concepts and Methods, M. Broy and C. B. Jones, Eds., Elsevier, Amsterdam, 1990. 33. David M. Goldschlag. "Proving Proof Rules: A Proof System for Concurrent Programs". Compass '90 (June 1990). 34. R. L. Goodstein. Recursive Number Theory. North-Holland Publishing Company, Amsterdam, 1964. 35. C. A. R. Hoare. "An Axiomatic Basis for Computer Programming". Comm. ACM 12, 10 (1969), 576-583. 36. L. Hodes. Solving Problems by Formula Manipulation. Proc. Second Inter. Joint Conf. on Art. Intell., The British Computer Society, 1971, pp. 553-559. 37. C.-H. Huang and C. Lengauer. "The Automated Proof of a Trace Transformation for a Bitonic Sort". Theoretical Computer Science 1, 46 (1986), 261-284. 38. W. A. Hunt. "Microprocessor Design Verification". Journal of Automated Reasoning 5, 4 (1989), 429-460. 39. Matt Kaufmann. A Formal Semantics and Proof of Soundness for the Logic of the NQTHM Version of the Boyer-Moore Theorem Prover. Internal Note 229, Institute for Computing Science, University of Texas at Austin, February, 1987. 40. Matt Kaufmann. A Mechanically-checked Semi-interactive Proof of Correctness of Gries's Algorithm for Finding the Largest Size of a Square True Submatrix. Internal Note 236, Institute for Computing Science, University of Texas at Austin, October, 1986. 41. Matt Kaufmann. An Example in NQTHM: Ramsey's Theorem. Internal Note 100, Computational Logic, Inc., November, 1988. 42. Matt Kaufmann. Boyer-Moore-ish Micro Gypsy and a Prototype Hardware Expander. Internal Note 73, Computational Logic, Inc., August, 1988. 43. Matt Kaufmann. A Mutual Recursion and Dependency Analysis Tool for NQTHM. Internal Note 99, Computational Logic, Inc., 1988. 44. Matt Kaufmann. A User's Manual for RCL. Internal Note 157, Computational Logic, Inc., October, 1989. 45. Matt Kaufmann and Matt Wilding. A Parallel Version of the Boyer-Moore Prover. Tech. Rept. 39, Computational Logic, Inc., February, 1989. 46. Matt Kaufmann. DEFN-SK: An Extension of the Boyer-Moore Theorem Prover to Handle First-Order Quantifiers. Tech. Rept. 43, Computational Logic, Inc., 1717 W. 6th St, Suite 290, Austin, Texas, June, 1989. 47. Matt Kaufmann. Addition of Free Variables to an Interactive Enhancement of the Boyer-Moore Theorem Prover. Tech. Rept. 42, Computational Logic, Inc., Austin, Texas, May, 1989. 48. Matt Kaufmann. A Mechanically-checked Correctness Proof for Generalization in the Presence of Free Variables. Tech. Rept. 53, Computational Logic, Inc., Austin, Texas, March, 1990. 49. Matt Kaufmann. An Integer Library for NQTHM. Internal Note 182, Computational Logic, Inc., March, 1990. 50. Leslie Lamport, Robert Shostak, and Marshall Pease. "The Byzantine Generals Problem". ACM TOPLAS 4, 3 (July 1982), 382-401. 51. C. Lengauer. "On the Role of Automated Theorem Proving in the Compile-Time Derivation of Concurrency". Journal of Automated Reasoning 1, 1 (1985), 75-101. 52. C. Lengauer and C.-H. Huang. A Mechanically Certified Theorem about Optimal Concurrency of Sorting Networks. Proc. 13th Ann. ACM Symp. on Principles of Programming Languages, 1986, pp. 307-317. 53. D. Loveland. Automated Theorem Proving: A Logical Basis. North Holland, Amsterdam, 1978. 54. J. McCarthy. "Recursive Functions of Symbolics Expressions and their Computation by Machine". Communications of the Association for Computing Machinery 3, 4 (1960), 184-195. 55. J. McCarthy. The Lisp Programmer's Manual. M.I.T. Computation Center, 1960. 56. J. McCarthy. Towards a Mathematical Science of Computation. Proceedings of IFIP Congress, 1962, pp. 21-28. 57. J. McCarthy. Computer Programs for Checking Mathematical Proofs. Recursive Function Theory, Proceedings of a Symposium in Pure Mathematics, Providence, Rhode Island, 1962, pp. 219-227. 58. J. McCarthy. A Basis for a Mathematical Theory of Computation. In Computer Programming and Formal Systems, P. Braffort and D. Hershberg, Eds., North-Holland Publishing Company, Amsterdam, The Netherlands, 1963. 59. J. McCarthy, et al. LISP 1.5 Programmer's Manual. The MIT Press, Cambridge, Massachusetts, 1965. 60. J S. Moore. "A Mechanical Proof of the Termination of Takeuchi's Function". Information Processing Letters 9, 4 (1979), 176-181. 61. J. S. Moore. "A Mechanically Verified Language Implementation". Journal of Automated Reasoning 5, 4 (1989), 461-492. 62. J. S. Moore, et. al. "Special Issue on System Verification". Journal of Automated Reasoning 5, 4 (1989), 409-530. 63. Matt Kaufmann. A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover. Tech. Rept. 19, Computational Logic, Inc., Austin, Texas, May, 1988. 64. Marshall Pease, Robert Shostak, and Leslie Lamport. "Reaching Agreement in the Presence of Faults". JACM 27, 2 (April 1980), 228-234. 65. J. A. Robinson. "A Machine-oriented Logic Based on the Resolution Principle". JACM 12, 1 (1965), 23-41. 66. David M. Russinoff. "An Experiment with the Boyer-Moore Theorem Prover: A Proof of Wilson's Theorem". Journal of Automated Reasoning 1, 2 (1985), 121-139. 67. N. Shankar. "Towards Mechanical Metamathematics". Journal of Automated Reasoning 1, 4 (1985), 407-434. 68. N. Shankar. A Mechanical Proof of the Church-Rosser Theorem. Tech. Rept. ICSCA-CMP-45, Institute for Computing Science, University of Texas at Austin, 1985. 69. N. Shankar. Proof Checking Metamathematics. Ph.D. Th., University of Texas at Austin, 1986. 70. J. R. Shoenfield. Mathematical Logic. Addison-Wesley, Reading, Ma., 1967. 71. T. Skolem. The Foundations of Elementary Arithmetic Established by Means of the Recursive Mode of Thought, without the Use of Apparent Variables Ranging over Infinite Domains. In From Frege to Godel, J. van Heijenoort, Ed., Harvard University Press, Cambridge, Massachusetts, 1967. 72. G. L. Steele, Jr. Common Lisp The Language. Digital Press, 30 North Avenue, Burlington, MA 01803, 1984. 73. J. von Neumann. Planning and Coding of Problems for an Electronic Computing Instrument, U.S. Army and Institute for Advanced Study report, 1946. In John von Neumann, Collected Works, Volume V, Pergamon Press, Oxford, 1961, pp. 34-235. 74. L. Wos, et al. "The concept of demodulation in theorem proving". Journal of the ACM 14 (1967), 698-709. 75. Matt Kaufmann and William D. Young. Comparing Gypsy and the Boyer-Moore Logic for Specifying Secure Systems. Institute for Computing Science, University of Texas at Austin, May, 1987. ICSCA-CMP-59. 76. W. D. Young. "A Mechanically Verified Code Generator". Journal of Automated Reasoning 5, 4 (1989), 493-518. 77. Yuan Yu. "Computer Proofs in Group Theory". Journal of Automated Reasoning (1990). To appear.