CLI Technical Reports and Notes

Reports are available as PostScript (PS), DVI or ASCII text format. Not all reports are available in all formats.

To obtain a copy of a report you will need to download one it the format you prefer, .ps, .dvi, or .pdf (if available). Not all reports may be distributed electronically. In such a case, one of the original authors may be able to help you.

You can also FTP the reports by looking at the files available via FTP.

Newly released (March 2004). Reports 102, 103, 120, and 121

A small number of notes are available as text files. Links are at the end of this page.

Reports
# Date Author(s) Title
124 5/97 Bevier, Young An Authorization Policy Language for Adage
123 5/97 Bevier, Young Principles of Authorization in Adage
122 11/96 Bevier, Ford, Simon, LSmith The Specification-Based Testing of A Trusted Kernel: MK++,
121 9/96 Bevier, Cohen An Executable Model of the Synergy File System, PS, PDF
120 9/96 Bevier, Cohen, Turner A Specification for the Synergy File System, PS, PDF
119 8/96 Boyer, Moore Mechanized Formal Reasoning about Programs and Computing Machines,
118 7/96 Brock, Kaufmann, Moore ACL2 Theorems about Commercial Microprocessors,
117 7/96 Brock, Kaufmann, Moore Heavy Inference: Theorems about Commercial Microprocessors (replaced by TR 118)
116 1/96 Young Interactive Consistency in ACL2
115 11/95 Moore, Kaufmann ACL2: An Industrial Strength Version of the Nqthm Logic
114 9/95 Mksmith, Akers AVA 95 Reference Manual, PS
113 9/95 Mksmith, Akers Annotated AVA 95 Reference Manual, PS
112 9/95 Mksmith A Formal Semantics for AVA 95, PS
111 7/95 Wilding, Young Specification and Verification of Real-time Executives (Part B: Specification and Proofs) (draft)
110 7/95 Wilding, Young Specification and Verification of Real-time Executives (Part A: Project Report) (draft)
109 5/95 Bevier, Young Developing an Abstract Separation Kernel via Successive Refinement (draft)
108 5/95 Young System Verification and the CLI Stack
107 4/95 Bevier, Cohen, Young Connection Policies and Controlled Interference
106 11/94 Hunt, Boyer, Albin, LSmith & Word A Study of the Feasibility of Verifying a Commercial DSP
105 10/94 Young, Bevier Mathematical Modeling and Analysis of an External Memory Manager
103 9/94 Bevier/LSmith A Mathematical Model of the Mach Kernel: Kernel Requests PS, PDF
102 9/94 Bevier/LSmith A Mathematical Model of the Mach Kernel PS, PDF
101 8/94 M. Kaufmann, J Moore Design Goals of ACL2 PS, DVI
100 8/94 M. Kaufmann, P Pecchiari (IRST, DIST) Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using 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
97 4/94 Kaufmann Combining an Interpreter-Based Approach to Software Verification with Verification Condition Generation PS
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
91 5/93 Carranza, Young A Fuzzy Controller: Theorems and Proofs about its Dynamic Behavior PS
90 1/95 Albin, Brock, Hunt, Smith Testing the FM9001 Microprocessor 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, Kaufmann The FM9001 Microprocessor Proof 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, Young Introduction to a Formally Defined 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, Kaufmann, Moore The Role of Automated Reasoning in Integrated System Verification 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, Young Middle Gypsy 2.05 Definition 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, PDF
44 5/89 Boyer, Goldschlag, Kaufmann, Moore Functional Instantiation in First Order Logic 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, Moore, Young An Approach to Systems Verification PS
40 3/89 Akers, Lsmith IDM - A Configuration Management Tool for Maintaining Consistency Through Incremental Development PS
39 2/89 Kaufmann, Wilding A Parallel Version of the Boyer-Moore Prover PS
37 1/89 Young A Mechanically Verified Code Generator PS, PDF
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, PDF
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, Craigen, Saaltink The nanoAVA Definition 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. See Robert Boyer and J S. Moore, A Computational Logic Handbook. Academic Press, New York, 1988.
17 12/87 Goldschlag, Crawford The Underlying Semantics of Transition Systems 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, Crawford The Mechanical Verification of 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, Young Toward Verified Execution Environments
4 5/86 Cohen Proving Gypsy Programs PS
This page is URL http://www.computationallogic.com/reports/index.html
Notes
# Date Author(s) Title
285 8/93 Kaufmann Several Approaches to the Correctness of a Simple Iterative Program with a Loop TXT
157 10/89 Kaufmann A User's Manual for RCL **DRAFT** TXT