### Technical Reports from Computational Logic Avaiable On-Line

Note: .ps versions of the .pdf files linked to below are also available here.

These postscript files were obtained from ftp://ftp.cli.com/pub/reports.

#114. M. Smith, Akers. AVA 95 Reference
Manual. 9/95.

#113. M. Smith, Akers. Annotated AVA 95
Reference Manual. 9/95.

#112. M. Smith. A Formal Semantics for AVA
95. 9/95.

#101. Kaufmann, Moore.
Design Goals of ACL2. 8/94.

#100. Kaufmann, Pecchiari. Interaction with
the Boyer-Moore Theorem Prover: A Tutorial Study Using the
Arithmetic-Geometric Mean Theorem. 8/94.

#99. Russinoff. Specification and
Verification of Gate-Level VHDL Models of Synchronous and Asynchronous
Circuits. 5/94.

#98. Russinoff. A Formalization of a Subset
of VHDL. 4/94.

#96. Akers. Strong Static Type Checking
for Functional Common Lisp. 12/93.

#95. Russinoff. A Formal Language for the
Specification and Verification of Synchronous and Asynchronous Circuits. 9/93.

#93. Young. Verifying a Simple Real-Time
System with Nqthm. 9/93.

#91. Carranza, Young. A Fuzzy Controller:
Theorems and Proofs about its Dynamic Behavior. 5/93.

#90. Albin, Brock, Hunt, L. Smith. Testing
the FM9001 Microprocessor. 1/95.

#89. Bevier, L. Smith. A Mathematical
Model of the Mach Kernel: Atomic Actions and Locks. 2/93.

#88. Bevier, L. Smith. A Mathematical
Model of the Mach Kernel: Entities and Relations. 2/93.

#86. Brock, Hunt, Kaufmann. The FM9001
Microprocessor Proof. 12/94.

#85. Kaufmann. An Assistant for Reading
Nqthm Proof Output. 11/92.

#84. Moore. Introduction to the BDD
Algorithm for the ATP Community. 10/92.

#83. Flatau. A Verified Implementation of
an Applicative Language with Dynamic Storage Allocation. 10/92.

#82. Carranza, Young. Verification of a
Fuzzy Controller. 9/92.

#81. Kaufmann. Quantification in Nqthm: a
Recognizer and Some Constructive Implementations. 8/92.

#79. Brock, Hunt. A Formal HDL and its use
in the FM9001 Verification. 7/92. pages in reverse order.

#78. Wilding. A Proved Application with
Simple Real-Time Properties. 10/92.

#77. Young. Verifying the Interactive
Convergence Clock Synchronization Algorithm Using the Boyer-Moore Theorem
Prover. 1/91.

#76. Brock, Hunt, Young. Introduction to a
Formally Defined Hardware Description Language. 4/92. pages in reverse order.

#75. Kaufmann. Response to FM91 Survey of
Formal Methods: Nqthm and Pc-Nqthm. 3/92.

#74. Flatau. A Compiler for NQTHM: A
Progress Report. 1/92.

#73. Good, Kaufmann, Moore. The Role of
Automated Reasoning in Integrated System Verification Environments. 1/92.

#72. Kaufmann, Moore. Should We Begin a
Standardization Process for Interface Logics? 1/92.

#71. Goldschlag. Mechanically verifying
Concurrent Programs. 9/91.

#70. Young. Verifiable Computer Security
and Hardware: Issues. 9/91.

#69. Moore. Mechanically Verified Hardware
Implementing an 8-Bit Parallel IO Byzantine Agreement Processor. 9/91.

#68. Moore. A Formal Model of Asynchronous
Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol. 8/91.

#67. Good, Young. Mathematical Methods for
Digital Systems Development. 8/91. pages in reverse order.

#66. Goldschlag. Verifying Safety and
Liveness Properties of Dela Insensitive Circuits. 3/91.

#65. Goldschlag. A Mechanical Formalization
of Several Fairness Notions. 3/91.

#64. M. Smith. The AVA Reference Manual:
Derived from ANSI/MIL-STD-1815A-1983. 2/92.

#62. Bevier, Young. Machine Checked Proofs
of a Byzantine Agreement Algorithm. 8/90.

#60. Brock, Hunt. A Formal Introduction to
a Simple Hardware Description Language. 7/90.

#59. Good, Siebert, Young. Middle Gypsy
2.05 Definition. 6/90.

#58. Basin, Kaufmann. The Boyer-Moore
Prover and Nuprl: An Experimental Comparison. 6/90. pages in reverse order.

#57. Bevier, Young. The Proof of
Correctness of a Fault-Tolerant Circuit Design. 6/90.

#56. Wilding. A Mechanically-Checked
Correctness Proof of a Floating-Point Search Program. 5/90.

#54. Boyer, Moore. A Theorem Prover for a
Computational Logic. 4/90.

#53. Kaufmann. A Mechanically-checked
Correctness Proof for Generalization in the Presence of Free Variables. 4/90.

#52. Hunt, Brock. The Formalization of a
Simple Hardware Description Language. 12/89.

#51. Bevier. The Partial Specification of
Microprocessor Instruction Set Architectures. 11/89.

#50. Goldschlag. The Verification of a
Minimum Node Algorithm. 10/89.

#49. Hunt. The Verification of a Bit- Slice
ALU. 9/89.

#48. Hunt. Microprocessor Design
Verification. 9/89.

#47. Good. Mathematical Forecasting. 9/89.

#46. Brock, Hunt. Report on the Formal
Specification and Partial Verification of the VIPER Microprocessor. 6/89.

#45. Young. Comparing Specification
Paradigms: Gypsy and Z. 6/89.

#44. Boyer, Goldschlag, Kaufmann, Moore.
Functional Instantiation in First Order Logic. 5/89. pages in reverse order.

#43. Kaufmann. DEFN-SK: An Extension of the
Boyer-Moore Theorem Prover to Handle First-Order Quantifiers. 6/89.

#42. Kaufmann. Addition of Free Variables
to the PC-NQTHM Interactive Enhancement of the Boyer-Moore Theorem Prover. 5/89.

#41. Bevier, Hunt, Moore, Young. An
Approach to Systems Verification. 4/89.

#40. Akers, L. Smith. IDM -- A
Configuration Management Tool for Maintaining Consistency Through Incremental
Development. 3/89.

#39. Kaufmann, Wilding. A Parallel Version
of the Boyer-Moore Prover. 2/89.

#37. Young. A Mechanically Verified Code
Generator. 1/89.

#36. Good. Mechanical Proofs About
Computer Programs. 11/88.

#33. Young. A Verified Code Generator. 11/88.

#32. Goldschlag. A Mechanically Verified
Proof System for Concurrent Programs. 1/89.

#30. Moore. A Mechanically Verified
Language Implementation. 9/88.

#28. Bevier. Kit: A Study In Operating
System Verification. 8/88.

#22. Moore. PITON: A Verified Assembly
Level Languages. 6/88.

#21. M. Smith, Craigen, Saaltink. The
nanoAVA Definition. 5/88.

#20. Good. Predicting Computer Behavior. 5/88.

#19. Kaufmann. A User's Manual for an
Interactive Enhancement to the Boyer-Moore Theorem Prover. 5/88.

#11. Bevier. A Verified Operating System
Kernel. 12/87.

#7. Goldschlag, Crawford. The Mechanical
Verification of Distributed Systems. 7/87.

#4. Cohen. Proving Gypsy Programs. 5/86.