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.