Note: .ps versions of the .pdf files linked to below are also available here. *An Nqthm Bibliography* We list below some works that may be of interest to users and students of Nqthm, the Boyer-Moore prover. Our list is certainly incomplete. We solicit contributions of new entries, any publicly available report about Nqthm, including applications of it. Send contributions to boyer@cs.utexas.edu. C. M. Angelo, D. Verkest, L. Claesen, and H. De Man. "On the Comparison of HOL and Boyer-Moore for Formal Hardware Verification". Formal Methods in System Design: An International Journal 2, 1 (1993), 45-72. S. Aujla and M. Fletcher. The Boyer-Moore Theorem Prover and LOTOS. In Formal Description Techniques, K. Turner, Ed., North-Holland, 1989. D. Basin and M. Kaufmann. The Boyer-Moore Prover and Nuprl: An Experimental Comparison. Tech. Rept. 58, Computational Logic, Inc., 1990. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/058.pdf]]. W. Bevier. A Verified Operating System Kernel. Ph.D. Th., University of Texas at Austin, 1987. University Microfilms and [[ftp://ftp.cs.utexas.edu/pub/boyer/diss/bevier.pdf]]. W. R. Bevier. A Library for Hardware Verification. Internal Note 57, Computational Logic, Inc., 1988. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-notes/note-057.pdf]]. W. R. Bevier. "Kit and the Short Stack". Journal of Automated Reasoning 5, 4 (1989), 519-530. W. R. Bevier. "Kit: A Study in Operating System Verification". IEEE Transactions on Software Engineering, 5, 11, (1989), 1382-1395. W. R. Bevier, W. A. Hunt, J S. Moore, and W. D. Young. "Special Issue on System Verification". Journal of Automated Reasoning 5, 4 (1989), 409-530. W. R. Bevier and L. Smith. A Mathematical Model of the Mach Kernel: Atomic Actions and Locks. Tech. Rept. 89, Computational Logic, Inc., 1993 [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/089.pdf]]. W. R. Bevier and L. Smith. A Mathematical Model of the Mach Kernel: Entities and Relations. Tech. Rept. 88, Computational Logic, Inc., 1993 [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/088.pdf]]. W. R. Bevier and W. D. Young. Machine Checked Proofs of a Byzantine Agreement Algorithm. Tech. Rept. 62, Computational Logic, Inc., 1990. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/062.pdf]]. W. R. Bevier and W. D. Young. The Proof of Correctness of a Fault-Tolerant Circuit Design. Tech. Rept. 57, Computational Logic, Inc., 1990. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/057.pdf]]. D. Borrione, L. Pierre, and P. Salem. "Formal Verification of VHDL Descriptions in the PREVAIL Environment". IEEE Design and Test Magazine 9, 2 (1992), 42-56. D. Borrione, L. Pierre, A. Salem. Formal Verification of VHDL Descriptions in Boyer-Moore: First Results. In J. Mermet, Ed., VHDL for Simulation, Synthesis and Formal Proofs, Kluwer, 1992. D. Borrione and H. Eveking. Formal Verification of Hardware Designs. Journal of the Brazilian Computer Society, Special Issue on Electronic Design Automation, November 1995. D. Borrione, H. Eveking, L. Pierre. Formal Proofs from HDL Descriptions. In J. Mermet, Ed., Fundamentals and Standards in Hardware Description Languages, Kluwer, 1993, pp. 155-193. D. Borrione, H. Bouamama, D. Deharbe, C. Le Faou, and A. Wahba. HDL-based Integration of Formal Methods and CAD Tools in the PREVAIL Environment. In International Conference on Formal Methods in Computer-Aided Design, Springer LNCS 1166, 1996, pp. 450-467. [[http://www-tima-vds.ujf-grenoble.fr/Publications/FMCAD-final-diff.ps]]. D. Borrione, H. Bouamama, and R. Suescun. Validation of the Numeric_Bit Package Using the NQTHM Theorem Prover. Proceedings of the APCHDL'96 Conference, Bangalore, India, 1996. R. S. Boyer. "Response, Biographical Sketch, and Photo on the Occasion of Receipt of the 1991 AMS Current Award for Automatic Theorem Proving". Notices of the American Mathematical Society 38, 5 (1991), 407-408. R. S. Boyer, D. M. Goldschlag, M. Kaufmann, and J S. Moore. Functional Instantiation in First-Order Logic. In V. Lifschitz, Ed., Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, 1991, pp. 7-26. 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 W. H. J. Feijen, A. J. M. van Gasteren, D. Gries, and J. Misra, Ed., Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra, Springer Texts and Monographs in Computer Science, 1990, pp. 54-66. R. S. Boyer, M. Kaufmann, and J S. Moore. "The Boyer-Moore Theorem Prover and Its Interactive Enhancement". Computers and Mathematics with Applications 29, 2 (1995), 27-62. R. S. Boyer and J S. Moore. "Proving Theorems about LISP Functions". Journal of the ACM 22, 1 (1975), 129-144. R. S. Boyer and J S. Moore. A Lemma Driven Automatic Theorem Prover for Recursive Function Theory. Proceedings of the 5th International Joint Conference on Artificial Intelligence, 1977, pp. 511-519. R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, New York, 1979. 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, Ed., Academic Press, London, 1981. 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, Ed., Academic Press, London, 1981. R. S. Boyer and J S. Moore. "Proof Checking the RSA Public Key Encryption Algorithm". American Mathematical Monthly 91, 3 (1984), 181-189. 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, Ed., American Mathematical Society, Providence, RI, 1984, pp. 133-167. R. S. Boyer and J S. Moore. "A Mechanical Proof of the Unsolvability of the Halting Problem". Journal of the ACM 31, 3 (1984), 441-458. 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, 2 (1988), 117-172. 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. R. S. Boyer and J S. Moore. A Theorem Prover for a Computational Logic. Keynote address, Automated Deduction -- CADE-10, Springer LNCS 449, 1990, pp. 1-15. R. S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, 1988. A second edition is slated for publication in 1997. This is the users' manual for Nqthm, the Boyer-Moore prover. However, this first (1988) edition is out of date, and the 1992 release of Nqthm includes supplementary documentation in subdirectory doc. The second edition will provide up-to-date documentation for the current release of Nqthm. R. S. Boyer and J S. Moore. MJRTY - A Fast Majority Vote Algorithm. In R. S. Boyer, Ed., Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer, 1991, pp. 105-117. R. S. Boyer and J S. Moore. Instructions for getting the `1992' release of Nqthm, the Boyer-Moore prover, which wasactually released in 1994, and then supplemented by further examples in 1995, may be found at [[ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html]]. The logic and the user commands may be found in directory "doc" of the release, and also here [[ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/logic-reference.text]]. The authoritative users guide to the 1992 release will be the second edition of A Computational Logic Handbook, Boyer and Moore, slated to be published by Academic Press in 1997. R. S. Boyer and Y. Yu. Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor. In Automated Deduction -- CADE-11, D. Kapur, Ed., Springer LNCS 607, 1992, pp. 416-430. R. S. Boyer and Y. Yu. A Formal Specification of Some User Mode Instructions for the Motorola 68020. Tech. Rept. TR-92-04, Computer Sciences Department, University of Texas at Austin, 1992. [[ftp://ftp.cs.utexas.edu/pub/techreports/tr92-04.ps]]. R. S. Boyer and Y. Yu. "Automated Correctness Proofs of Machine Code Programs for a Widely Used Microprocessor". Journal of the ACM 43, 1 (1996), 166-192. J. D. Bright, G. F. Sullivan, and G. M. Mason. "A Formally Verified Sorting Certifier". To appear in IEEE Transactions on Computers. [[http://www.dnai.com/~bright/pubs/sorting.ps]]. B. Brock, W. A. Hunt, and M. Kaufmann. The FM9001 Microprocessor Proof. Tech. Rept. 86, Computational Logic, Inc., 1994. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/086.pdf]]. Although it is far afield from formal verification, those interested in more traditional ``verification'' may enjoy: K. Albin, B. Brock, W. A. Hunt, and L. Smith. Testing the FM9001 Microprocessor. Tech. Rept. 90, Computational Logic, Inc., 1995. ="ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/090.pdf"> ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/090.pdf. See also ftp://ftp.cs.utexas.edu/pub/boyer/fm9001/index.html for some more information about the FM9001, including pictures. B. Brock, W. A. Hunt, and W. D. Young. Introduction to a Formally Defined Hardware Description Language. In V. Stavridou, T. Melham, and R. Boute, Ed., Theorem Provers in Circuit Design, North-Holland, 1992, pp. 3-35. 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. A. Bronstein. MLP: String-functional Semantics and Boyer-Moore Mechanization for the Formal Verification of Synchronous Circuits. Ph.D. Th., Stanford University, 1989. 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, 1989, pp. 317-333. A. Bronstein and C. Talcott. Formal Verification of Pipelines based on String-Functional Semantics. IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, 1989. M. Carranza and W. D. Young. Verification of a Fuzzy Controller. Tech. Rept. 82, Computational Logic, Inc., 1992. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/082.pdf]]. M. Carranza and W. D. Young. A Fuzzy Controller: Theorems and Proofs about its Dynamic Behavior. Tech. Rept. 91, Computational Logic, Inc., 1993. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/091.pdf]]. J. Cook and S. Subramanian. A Formal Semantics for C in Nqthm. Technical Report 517D, Trusted Information Systems, October, 1994. {{http://www.tis.com/docs/research/assurance/ps/nqsem.ps}}. J. R. Cowles. Using NQTHM to Verify Insert, Search, and Traversal Functions for Search Trees, Internal Note 241, Computational Logic, Inc., 1991. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-notes/note-241.pdf]]. J. R. Cowles. Meeting a Challenge of Knuth, Internal Note 286, Computational Logic, Inc., 1993. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-notes/note-286.txt]]. B. L. Di Vito. Verification of Communications Protocols and Abstract Process Models. Ph.D. Th., University of Texas at Austin, 1982. University Microfilms. J. Dushina and D. Borrione. Formalisation and Validation of the Std_Logic_1164 and Numeric_Std VHDL Packages Using the Nqthm Theorem Prover. 2nd Workshop on Libraries, Component Modeling and Quality Assurance, Toledo, Spain, 23-25 April 1997. [[http://www-tima-vds.ujf-grenoble.fr/Publications/LCMQA97.ps]]. A. Flatau. A Verified Implementation of an Applicative Language with Dynamic Storage Allocation. Ph.D. Th., University of Texas at Austin, 1992. University Microfilms and [[ftp://ftp.cs.utexas.edu/pub/boyer/diss/flatau.pdf]]. S. M. German and Y. Wang. Formal Verification of Parameterized Hardware Designs. International Conference on Computer Design, 1985. Reprinted in M. Yoeli, (Ed.), Formal Verification of Hardware Design, IEEE Computer Society Press Tutorial, 1990. P. Y. Gloess. An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions. In 5th Conference on Automated Deduction, Springer LNCS 87, 1980, pp. 154-169. D. M. Goldschlag. Mechanizing Unity. In Programming Concepts and Methods, M. Broy and C. B. Jones, Ed., North Holland, Amsterdam, 1990. D. M. Goldschlag. "Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover". IEEE Transactions on Software Engineering 16 (September 1990). D. M. Goldschlag. Mechanically Verifying Concurrent Programs. Ph.D. Th., University of Texas at Austin, 1992. University Microfilms and [[ftp://ftp.cs.utexas.edu/pub/boyer/diss/goldschlag.pdf]]. D. M. Goldschlag. A Mechanization of Unity in PC-Nqthm. Journal of Automated Reasoning. Vol. 23 No. 3-4. November 1999. D. I. Good, A. Siebert, and W. D. Young. Middle Gypsy 2.05 Definition. Tech. Rept. 59, Computational Logic, Inc., 1990. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/059.pdf]]. D. Good, M. Kaufmann, and J Moore. The Role of Automated Reasoning in Integrated System Verification Environments. Tech. Rept. 73, Computational Logic, Inc., 1992. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/073.pdf]]. C.-H. Huang and C. Lengauer. "The Automated Proof of a Trace Transformation for a Bitonic Sort". Theoretical Computer Science 1 (1986), 261-284. W. A. Hunt. FM8501: A Verified Microprocessor. Ph.D. Th., University of Texas at Austin, 1985. University Microfilms. Published as Hunt's 1994 reference below. W. A. Hunt. The Mechanical Verification of a Microprocessor Design. In From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione, Ed., North Holland, 1987, pp. 89-132. Reprinted in M. Yoeli, (Ed.), Formal Verification of Hardware Design, IEEE Computer Society Press Tutorial, 1990, pp. 20-30. W. A. Hunt. "Microprocessor Design Verification". Journal of Automated Reasoning 5, 4 (1989), 429-460. W. A. Hunt and B. Brock . "A Formal HDL and Its Use in the FM9001 Verification". Philosophical Transactions of the the Royal Society, Series A 339 (1992). Reprinted in Mechanized Reasoning and Hardware Design, C. Hoare and M. Gordon, eds., Prentice Hall, pp. 35-47, 1992. W. A. Hunt. FM8501: A Verified Microprocessor. Springer LNCS 795, 1994. M. Kaufmann. A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover. Tech. Rept. 19, Computational Logic, Inc., May, 1988. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/019.pdf]]. M. Kaufmann. Addition of Free Variables to an Interactive Enchancement of the Boyer-Moore Theorem Prover. Tech. Rept. 42, Computational Logic, Inc., 1990. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/042.pdf]]. M. Kaufmann. An Instructive Example for Beginning Users of the Boyer-Moore Theorem Prover. Internal Note 185, Computational Logic, Inc., 1990. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-notes/note-185.pdf]]. M. Kaufmann. An Integer Library for Nqthm. Internal Note 182, Computational Logic, Inc., 1990. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-notes/note-182.pdf]]. M. Kaufmann. An Example in Nqthm: Ramsey's Theorem. Internal Note 100, Computational Logic, Inc., 1991, [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-notes/note-100.pdf]]. M. Kaufmann. "Generalization in the Presence of Free Variables: A Mechanically-Checked Proof for One Algorithm". Journal of Automated Reasoning 7, 1 (March 1991), 109-158. M. Kaufmann. A Simple Example for Nqthm: Modeling Locking. Internal Note 216, Computational Logic, Inc., 1991. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-notes/note-216.pdf]]. M. Kaufmann. Response to FM91 Survey of Formal Methods: Nqthm and Pc-Nqthm. Tech. Rept. 75, Computational Logic, Inc., 1992. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/075.pdf]]. M. Kaufmann. An Assistant for Reading Nqthm Proof Output. Tech. Rept. 85, Computational Logic, Inc., May, 1992 [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/085.pdf]]. M. Kaufmann. Quantification in Nqthm: a Recognizer and Some Constructive Implementations. Tech. Rept. 81, Computational Logic, Inc., 1992 [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/081.pdf]]. M. Kaufmann. "An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification". Journal of Automated Reasoning 9, 3 (December 1992), 355-372. M. Kaufmann and P. Pecchiari. "Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem". Journal of Automated Reasoning 16, 1-2 (1996), 181-222. M. Kim. On Automatically Generating and Using Examples in a Computational Logic System. Ph.D. Th., University of Texas at Austin, 1986. University Microfilms and [[ftp://ftp.cs.utexas.edu/pub/boyer/diss/kim.pdf]]. K. Kunen. "A Ramsey Theorem in Boyer-Moore Logic". Journal of Automated Reasoning 15 (1995), 217-235. K. Kunen. "Non-constructive Computational Mathematics." Journal of Automated Reasoning, 21 (1998) 69-97. 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. C. Lengauer and C.-H. Huang. A Mechanically Certified Theorem about Optimal Concurrency of Sorting Networks. Proceedings of the 13th Annual Symposium on Principles of Programming Languages (POPL '86), ACM, 1986, 307-317. Also Tech. Rept. TR-85-23, Department of Computer Sciences, The University of Texas at Austin, Oct., 1985. W. McCune. A Proof-checker for resolution/paramodulation proofs. 1995. Mathematics and Computer Science Division, Argonne National Laboratory, 1995. [[ftp://info.mcs.anl.gov/pub/Otter/QED/check-4.tar.gz]]. J S. Moore. "Introducing Iteration into the Pure LISP Theorem-Prover." IEEE Transactions on Software Engineering, 1, 3 (1975), 328-338. J S. Moore. "A Mechanical Proof of the Termination of Takeuchi's Function". Information Processing Letters 9, 4 (1979), 176-181. J S. Moore. Mechanically Verified Hardware Implementing an 8-Bit Parallel IO Byzantine Agreement Processor. Tech. Rept. 69, Computational Logic, Inc., 1991. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/069.pdf]]. J S. Moore. "Response, Biographical Sketch, and Photo on the Occasion of Receipt of the 1991 AMS Current Award for Automatic Theorem Proving". Notices of the American Mathematical Society 38, 5 (1991), 408-410. J S. Moore. "A Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol". Formal Aspects of Computing 6, 1 (1994), 60-91. J S. Moore. Piton: A Mechanically Verified Assembly-Level Language. Kluwer, 1996. M. Nagayama and C. Talcott. An NQTHM Mechanization of ``An Exercise in the Verification of Multi-Process Programs''. Tech. Rept. STAN-CS-91-1370, Computer Science Department, Stanford University, 1991. F. Nicoli and L. Pierre. Formal Verification of Behavioural VHDL Specifications : A Case Study. Proceedings of the International Conference EURO-DAC with EURO-VHDL, 1994. L. Pierre. VHDL Description and Formal Verification of Systolic Multipliers. In D. Agnew and L. Claesen, Ed., Computer Hardware Description Languages and their Applications, North Holland, 1993. L. Pierre. Describing and Verifying Synchronous Circuits with the Boyer-Moore Theorem Prover. In P. Camurati and H. Eveking, Ed., Correct Hardware Design and Verification Methods, Springer LNCS 987, 1995. L. Pierre. An Automatic Generalization Method for the Inductive Proof of Replicated and Parallel Architectures. In R. Kumar and T. Kropf, Ed., Theorem Provers in Circuit Design, Springer LNCS 901, 1995. L. Pierre. VHDL Description, Boyer-Moore Specification and Formal Verification of a Parallel System for Finding a Maximum. Proceedings of a Workshop on Formal Methods for Parallel Programming : Theory and Applications, 1997. J. D. Ramsdell. The Tail Recursive SECD Machine. Published on the Internet, 1997, [[ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/trsecd/trsecd.html]]. S. Read. Formal Methods for VLSI Design. Ph.D. Th., University of Manchester Institute of Science and Technology, 1994. S. Read and M. Edwards. A Formal Semantics of VHDL in Boyer-Moore Logic. Proceedings of the International Conference on Concurrent Engineering and Electronic Design Automation, Poole, Great Britain, 1994, pp. 395-400. D. M. Russinoff. A Mechanical Proof of Wilson's Theorem. Master Th., University of Texas at Austin,1983. D. 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. D. M. Russinoff. "A Mechanical Proof of Quadratic Reciprocity". Journal of Automated Reasoning 8, 1 (1992), 3-21. D. M. Russinoff. "Verifying Concurrent Programs with the Boyer-Moore Prover". Formal Aspects of Computing 5 (1992), 597-611. D. M. Russinoff. "A Mechanically Verified Incremental Garbage Collector". Formal Aspects of Computing 6 (1994), 359-390. [[http://www.onr.com/user/russ/david/igc.html]]. D. M. Russinoff. Specification and Verification of Gate-Level VHDL Models of Synchronous and Asynchronous Circuits. In E. Boerger, Ed., Specification and Validation Methods, Oxford University Press, 1995. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/099.pdf]]. D. M. Russinoff. "A Formalization of a Subset of VHDL". Formal Methods in System Design 7 (1995), 7-25. In special issue on VHDL Semantics. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/098.pdf]]. J. L. Ruiz Reina, J.A. Alonso, M.J. Hidalgo, and F.J. Martin. "Mechanical verification of rule-based unification algorithm in the Boyer-Moore theorem prover". Proceedings of the Joint Conference on Declarative Programming, AGP'99 (1999), pp. 289-304. [[ http://www-cs.us.es/~jruiz/fot-nqthm]] A. Salem and D. Borrione. Formal Semantics of VHDL Timing Constructs. In J. Mermet, Ed., VHDL for Simulation, Synthesis and Formal Proofs of Hardware, Kluwer, 1992, pp. 195-206. N. Shankar. "Towards Mechanical Metamathematics". Journal of Automated Reasoning 1, 4 (1985), 407-434. N. Shankar. Proof Checking Metamathematics. Ph.D. Th., University of Texas at Austin, 1986. Published as Shankar's 1994 reference below. University Microfilms. N. Shankar. "A Mechanical Proof of the Church-Rosser Theorem". Journal of the ACM 35, 3 (1988), 475-522. N. Shankar. Metamathematics, Machines, and Goedel's Proof. Cambridge University Press, 1994. S. Subramanian. A Mechanized Framework for Specifying Problem Domains and Verifying Plans. Ph.D. Th., University of Texas at Austin, 1993. University Microfilms and [[ftp://ftp.cs.utexas.edu/pub/boyer/diss/subramanian.pdf]]. S. Subramanian. "An Interactive Solution to the n x n Mutilated Checkerboard Problem". Journal of Logic and Computation 6, 4 (1996), 573-598. S. Subramanian and J. Cook. Automatic Verification of Object Code Against Source Code Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS'96), June, 1996, pp. 46-55. [[http://www.tis.com/docs/research/assurance/ps/compass96-final.ps]]. S. Subramanian and J. Cook. Mechanical Verification of C Programs. Proceedings of the ACM SIGSOFT Workshop on Formal Methods in Software Practice, January, 1996. [[://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6V1X-3VGTB2B-4&_user=108429&_coverDate=01%2F31%2F1999&_alid=1149382&_rdoc=1&_fmt=full&_orig=search&_cdi=5686&_acct=C000004378&_version=1&_urlVersion=0&_userid=108429&md5=12f9ac88303ff6a222002d5ee4c10bca"> Via Science Direct]]. D. Verkest, L. Claesen, and H. De Man. On the Use of the Boyer-Moore Theorem Prover for Correctness Proofs of Parameterized Hardware Modules. In Formal VLSI Specification and Synthesis, L. Claesen, Ed., Elsevier, 1990, pp. 99-116. D. Verkest, L. Claesen, and H. De Man. Correctness Proofs of Parameterized Hardware Modules in the Cathedral-II Synthesis Environment. Proceedings of the European Design Automation Conference, EDAC 1990. pp. 62-66. D. Verkest, L. Claesen, and H. De Man. A Proof of the Non-Restoring Division Algorithm and its Implementation on the Cathedral-II ALU. In Designing Correct Circuits, J. Staunstrup and R. Sharp, Ed., Elsevier, pp. 173-192. D. Verkest, J. Vandenbergh, L. Claesen, and H. De Man. A Description Methodology for Parameterized Modules in the Boyer-Moore Logic. In Theorem Provers in Circuit Design: Theory, Practice and Experience, V. Stavridou, T. Melham, and R. Boute, Ed., Elsevier, pp. 37-57. D. Verkest, L. Claesen, and H. De Man. Proof of the Non-Restoring Division Algorithm and its Implementation on an ALU. Journal of Formal Methods in System Design. 4, 1 (1994), 5-31. D. Weber-Wulff. "Proof Movie : A Proof with the Boyer-Moore Prover". Formal Aspects of Computing 5 (1993), 121-151. D. Weber-Wulff. Contributions to Mechanical Proofs of Correctness for Compiler Front-Ends. Ph.D. Th., University of Kiel, Germany, Department of Computer Science, 1997. Technical Report IfI 9707. M. Wilding. A Mechanically-Checked Correctness Proof of a Floating-Point Search Program. Tech. Rept. 56, Computational Logic, Inc., 1990. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/056.pdf]]. M. Wilding. "Proving Matijasevich's Lemma with a Default Arithmetic Strategy". Journal of Automated Reasoning 7, 3 (1991), 439-446. M. Wilding. A Proved Application with Simple Real Time Properties. Tech. Rept. 78, Computational Logic, Inc., 1992. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/078.pdf]]. M. Wilding. A Mechanically Verified Application for a Mechanically Verified Environment. Computer-Aided Verification -- CAV '93, Springer LNCS 697, 1993. [[wilding-cav93.pdf]]. M. Wilding. Machine-Checked Real-Time System Verification. Ph.D. Th., University of Texas at Austin, May 1996. University Microfilms, [[ftp://ftp.cs.utexas.edu/pub/boyer/diss/wilding.pdf]], and [[ftp://ftp.cs.utexas.edu/pub/boyer/diss/wilding-diss-events.tar.gz]] M. Wilding. A Detailed Processor Model for Verification of Real-time Applications. In T. Hilburn, G. Suski, and J. Zalewski, Ed., 2nd IFAC Workshop on Safety and Reliability in Emerging Control Technologies, Pergamon/Elsevier Science, 1996. M. Wilding. Robust Computer System Proofs in PVS. In LFM97: Fourth NASA Langley Formal Methods Workshop, C. Michael Holloway and Kelly J. Hayhurst, eds. NASA Conference Publication, 1997. [[ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/wilding-nasa-workshop.pdf]]. M. Wilding. A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy. CAV '98, Alan J. Hu and Moshe Y. Vardi, eds. Springer-Verlag Lecture Notes in Computer Science 1427, 1998, pp. 369-378, [[http://home.plutonium.net/~hokie/docs/cav98.ps]]. W. D. Young. A Verified Code-Generator for a Subset of Gypsy. Ph.D. Th., University of Texas at Austin, 1988. University Microfilms and [[ftp://ftp.cs.utexas.edu/pub/boyer/diss/young.pdf]]. W. D. Young. A Simple Expression Compiler: A Programming and Proof Example for an Nqthm Course. Internal Note 210, Computational Logic, Inc., 1990. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-notes/note-210.pdf]]. W. D. Young. Verifying the Interactive Convergence Clock Synchronization Algorithm Using the Boyer-Moore Theorem Prover. Tech. Rept. 77, Computational Logic, Inc., 1991. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/077.pdf]]. W. D. Young. Modeling and Verification of a Simple Real-Time Gate Controller. In M. Hinchey and J. Bowen, Ed., Applications of Formal Methods, Prentice-Hall, 1994. [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/093.pdf]]. Y. Yu. "Computer Proofs in Group Theory". Journal of Automated Reasoning 6, 3 (1990). Y. Yu. Automated Proofs of Object Code for a Widely Used Microprocessor. Ph.D. Th., University of Texas at Austin, 1992. University Microfilms and [[ftp://ftp.cs.utexas.edu/pub/boyer/diss/yu.pdf]]. Examples distributed with Nqthm. More than 16 megabytes of example input to Nqthm, in more than 140 files, may be found under the directory [[ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-1992/examples]]. Many of these examples are documented in the references above. All of these examples are briefly described in Chapter 14 of the second edition of A Computational Logic Handbook, Boyer and Moore, Academic Press, 1998. The examples range dramatically in scope, from very simple tutorial examples in elementary list and number theory to multi-year projects in computer system verification. Related reports on verification may be found at o UT ICS Reports [[ftp://ftp.cs.utexas.edu/pub/boyer/ics-reports/index.html]] o CLI Reports [[ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/index.html]] [[Main page.]]