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.
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.
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
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

**Main
page.**