----------------------------------------------------------------------- NOTE: This file is an index of CLI Technical Reports intended for FTP users. It is a TEXT version of the WWW index page, which is at the following URL http://www.cli.com/reports ----------------------------------------------------------------------- Computational Logic, Inc. CLI Technical Reports Click on abstracts to see the report abstracts. To obtain a copy of a report, do one of the following: 1. Each report may be available as PostScript, DVI or ASCII text format. Not all reports are available in all formats. Click on the desired type of format to obtain the report: PS == PostScript DVI == TeX DVI Text == ASCII text 2. Fill out the order form at the end of this page 3. Send a request, including your mailing address and the technical report title and number, to www-tech-reports@cli.com 4. Send mail to the following address: Computational Logic, Inc. Attn: Publications 1717 West Sixth St., Suite 290 Austin, Texas 78703-4776 You can also FTP the DVI or PS versions of these reports by looking at the files available via FTP. You can view the DVI or PS versions of these reports by clicking on the highlighted report number. [Image] Home # Date Author(s) Title ------------------------------------------------------------------- 101 8/94 M. Kaufmann, Design Goals of ACL2 J Moore PS, DVI 100 8/94 M. Kaufmann, Interaction with the Boyer-Moore P Pecchiari Theorem Prover: A Tutorial Study Using (IRST, DIST) the Arithmetic-Geometric Mean Theorem PS, DVI 99 5/94 Russinoff Specification and Verification of Gate-Level VHDL Models of Synchronous and Asynchronous Circuits. PS, DVI 98 4/94 Russinoff A Formalization of a Subset of VHDL PS, DVI 96 12/93 Akers Strong Static Type Checking for Functional Common Lisp PS 95 9/93 Russinoff A Formal Language for the Specification and Verification of Synchronous and Asynchronous Circuits PS, DVI 94 10/93 Bevier/Young A State-Based Approach to Noninterference 93 9/93 Young Verifying a Simple Real-Time System with Nqthm PS, DVI 92 5/93 Yuan Yu Automated Proofs of Object Code for a Widely Used Microprocessor (Vol I, 114 pages, Vol. II, 619 pages. There is $60.00 charge for hard copy of Vol. II.) PS, DVI 90 1/95 Albin/Brock/ Testing the FM9001 Microprocessor Hunt/Smith PS 91 5/93 Carranza/Young A Fuzzy Controller: Theorems and Proofs about its Dynamic Behavior PS 89 2/93 Bevier/LSmith A Mathematical Model of the Mach Kernel: Atomic Actions and Locks PS, DVI 88 2/93 Bevier/LSmith A Mathematical Model of the Mach Kernel: Entities and Relations PS, DVI 86 12/94 Brock/Hunt/ The FM9001 Microprocessor Proof Kaufmann PS 85 11/92 Kaufmann An Assistant for Reading Nqthm Proof Output PS 84 10/92 Moore Introduction to the BDD Algorithm for the ATP Community PS 83 10/92 Flatau A Verified Implementation of an Applicative Language with Dynamic Storage Allocation PS, DVI 82 9/92 Carranza/Young Verification of a Fuzzy Controller PS 81 8/92 Kaufmann Quantification in Nqthm: a Recognizer and Some Constructive Implementations PS 79 7/92 Brock/Hunt A Formal HDL and its use in the FM9001 Verification PS, DVI 78 10/92 Wilding A Proved Application with Simple Real-Time Properties PS, DVI 77 1/91 Young Verifying the Interactive Convergence Clock Synchronization Algorithm Using the Boyer-Moore Theorem Prover PS 76 4/92 Brock/Hunt/ Introduction to a Formally Defined Young Hardware Description Language PS, DVI 75 3/92 Kaufmann Response to FM91 Survey of Formal Methods: Nqthm and Pc-Nqthm PS 74 1/92 Flatau A Compiler for NQTHM: A Progress Report PS 73 1/92 Good/ The Role of Automated Reasoning Kaufmann/ in Integrated System Verification Moore Environments PS 72 1/92 Kaufmann/Moore Should We Begin a Standardization Process for Interface Logics? PS 71 9/91 Goldschlag Mechanically verifying Concurrent Programs PS 70 9/91 Young Verifiable Computer Security and Hardware: Issues PS 69 9/91 Moore Mechanically Verified Hardware Implementing an 8-Bit Parallel IO Byzantine Agreement Processor PS 68 8/91 Moore A Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol PS 67 8/91 Good/Young Mathematical Methods for Digital Systems Development PS, DVI 66 3/91 Goldschlag Verifying Safety and Liveness Properties of Dela Insensitive Circuits PS 65 3/91 Goldschlag A Mechanical Formalization of Several Fairness Notions PS 64 2/92 M. K. Smith The AVA Reverence Manual: Derived from ANSI/MIL-STD-1815A-1983 PS 62 8/90 Bevier/Young Machine Checked Proofs of a Byzantine Agreement Algorithm PS 60 7/90 Brock/Hunt A Formal Introduction to a Simple Hardware Description Language PS, DVI 59 6/90 Good/Siebert/ Middle Gypsy 2.05 Definition Young PS 58 6/90 Basin/Kaufmann The Boyer-Moore Prover and Nuprl: An Experimental Comparison PS, DVI 57 6/90 Bevier/Young The Proof of Correctness of a Fault-Tolerant Circuit Design PS 56 5/90 Wilding A Mechanically-Checked Correctness Proof of a Floating-Point Search Program PS 54 4/90 Boyer/Moore A Theorem Prover for a Computational Logic PS 53 4/90 Kaufmann A Mechanically-checked Correctness Proof for Generalization in the Presence of Free Variables PS 52 12/89 Hunt/ Brock The Formalization of a Simple Hardware Description Language PS 51 11/89 Bevier The Partial Specification of Microprocessor Instruction Set Architectures PS 50 10/89 Goldschlag The Verification of a Minimum Node Algorithm PS 49 9/89 Hunt The Verification of a Bit- Slice ALU PS 48 9/89 Hunt Microprocessor Design Verification PS 47 9/89 Good Mathematical Forecasting PS 46 6/89 Brock/Hunt Report on the Formal Specification and Partial Verification of the VIPER Microprocessor. PS, DVI 45 6/89 Young Comparing Specification Paradigms: Gypsy and Z PS 44 5/89 Boyer/ Functional Instantiation in First Order Logic Goldschlag/ Kaufmann/Moore PS, DVI 43 6/89 Kaufmann DEFN-SK: An Extension of the Boyer-Moore Theorem Prover to Handle First-Order Quantifiers PS 42 5/89 Kaufmann Addition of Free Variables to the PC-NQTHM Interactive Enhancement of the Boyer-Moore Theorem Prover PS 41 4/89 Bevier/Hunt/ An Approach to Systems Verification Moore/Young PS 40 3/89 Akers/Lsmith IDM -- A Configuration Management Tool for Maintaining Consistency Through Incremental Development PS 39 2/89 Kaufmann/ A Parallel Version of the Boyer-Moore Prover Wilding PS 37 1/89 Young A Mechanically Verified Code Generator PS 36 11/88 Good Mechanical Proofs About Computer Programs PS 35 11/88 Young Report on Middle Gypsy PS 34 11/88 Young Report on Micro-Gypsy PS 33 11/88 Young A Verified Code Generator PS 32 1/89 Goldschlag A Mechanically Verified Proof System for Concurrent Programs. PS 30 9/88 JMoore A Mechanically Verified Language Implementation PS 28 8/88 Bevier Kit: A Study In Operating System Verification PS 25 6/88 Boyer, Moore Basic Events for A Computational Logic (416 pages) See "events.lisp" in NQTHM-1992 FTP area. 24 6/88 Boyer, Moore The Code for A Computational Logic (515 pages) See "code*.lisp" in NQTHM-1992 FTP area. 22 6/88 J Moore PITON: A Verified Assembly Level Languages PS 21 5/88 MKSmith/ The nanoAVA Definition Craigen/ Saaltink PS 20 5/88 Good Predicting Computer Behavior PS 19 5/88 Kaufmann A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover PS 18 2/88 Boyer/Moore The User's Manual for a Computational Logic 17 12/87 Goldschlag/ The Underlying Semantics of Transition Systems Crawford PS 16 12/87 Bevier The Formal Specification and Definition of KIT PS 11 12/87 Bevier A Verified Operating System Kernel PS 9 4/87 Shankar Proof Checking Metamathematics Vols. I and II (570 pages) See "Metamathematics, Machines, and Goedel's Proof", N. Shankar, Cambridge University Press, 1994. 7 7/87 Goldschlag/ The Mechanical Verification of Crawford Distributed Systems PS 6 87 Hunt The Mechanical Verification of a Microprocessor Design See "FM8501: A Verified Microprocessor.", W. Hunt, LNCS 795, Springer-Verlag, 1994. 5 2/87 Hunt/Bevier/ Toward Verified Execution Young Environments 4 5/86 Cohen Proving Gypsy Programs PS ---------------------------------------------------------------------------- CLI Technical Report Order Form Name Mail Stop Organization Street1 Street2 City State Country Zip Reports you would like: Number Title 1. 2. 3. 4. 5. 6. ---------------------------------------------------------------------------- [Image] Home This page is URL http://www.cli.com/reports/index.html