101. Design Goals of ACL2, by Matt Kaufmann and J Strother Moore. August, 1994, 41 pages.
ACL2 is a theorem proving system under development at Computational Logic, Inc., by the authors of the Boyer-Moore system, Nqthm, and its interactive enhancement, Pc-Nqthm, based on our perceptions of some of the inadequacies of Nqthm when used in large-scale verification projects. The logic of ACL2 is based on the applicative subset of Common Lisp. By adding to the applicative subset of Common Lisp a single-threaded notion of state, fast applicative arrays and property lists, and efficiently implemented multiple values, an efficient and practical applicative programming language is produced. By axiomatizing the primitives and introducing appropriate rules of inference and extension principles, that language can be turned into a logic. A premise of the ACL2 Project is that the Nqthm proof heuristics allow the mechanization of the discovery of proofs in the ACL2 logic with the same degree of success that Nqthm has for its logic. The ACL2 system may be viewed as an extended re-implementation of Nqthm for extended applicative Common Lisp. ACL2 is written using the logic it supports. We discuss the inadequacies of Nqthm motivating the design of ACL2; we briefly describe the ACL2 logic, theorem prover, interface, implementation, and some applications; and we discuss some of our concerns and misgivings about the current design. Because ACL2 is not yet ready for public distribution, we make no claims as to its superiority to Nqthm or other theorem proving systems.
100. Interaction with the Boyer-Moore and Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem, by Matt Kaufmann (CLI) and Paolo Pecchiari (IRST, DIST). August, 1994, 115 pages.
There are many papers describing problems solved using the Boyer-Moore theorem prover, as well as papers describing new tools and functionalities added to it. Unfortunately, so far, there has been no tutorial paper describing typical interactions that a user has with this system when trying to solve a nontrivial problem, including a discussion of issues that arise in these situations. In this paper we aim to fill this gap by illustrating how we have proved an interesting theorem with the Boyer-Moore theorem prover: a formalization of the assertion that the arithmetic mean of a sequence of natural numbers is greater than or equal to their geometric mean. We hope that this report will be of value not only for (non-expert) users of this system, who can learn some approaches (and tricks) to use when proving theorems with it, but also for implementors of automated deduction systems. Perhaps our main point is that, at least in the case of Nqthm, the user can interact with the system without knowing much about how it works inside. This perspective suggests the development of theorem provers that allow interaction that is user oriented and not system developer oriented.
99. Specification and Verification of Gate-Level VHDL Models of Synchronous and Asynchronous Circuits by David Russinoff. May 10, 1994, 54 pages.
We present a mathematical definition of a hardware description language (HDL) that admits a semantics-preserving translation to a subset of VHDL. Our HDL includes the basic VHDL propagation delay mechanisms and gate-level circuit descriptions. We also develop formal procedures for deriving and verifying concise behavioral specifications of combinational and sequential devices. The HDL and the specification procedures have been formally encoded in the computational logic of Boyer and Moore, which provides a LISP implementation as well as a facility for mechanical proof-checking. As an application, we design, specify, and verify a circuit that achieves asynchronous communication by means of the biphase mark protocol.
98. A Formalized of a Subset of VHDL, by David M. Russinoff. April 28, 1994. 22 pages.
We present a mathematical definition of a hardware description language that admits a semantics-preserving translation to a subset of VHDL. The language is based on the VHDL model of event-driven simulation and includes behavioral and structural circuit descriptions, the basic VHDL propagation delay mechanisms, and both zero and nonzero delays. It has been formally encoded in the computational logic of Boyer and Moore, which provides a LISP implementation as well as a facility for mechanical proof-checking. We prove a number of basic properties of the simulator, which we apply to the analysis of gate-level designs of a one-bit adder and a d-flip-flop.
96. Strong Static Type Checking for Functional Common Lisp, Robert L. Akers.
This thesis presents a type system which supports the strong static type checking of programs developed in an applicative subset of the Common Lisp language. The Lisp subset is augmented with a guard construct for function definitions, which allows type restrictions to be placed on the arguments. Guards support the analysis and safe use of partial functions, like CAR, which are well-defined only for arguments of a certain type.
95. A Formal Language for the Specification and Verification of Synchronous and Asynchronous Circuits, David M. Russinoff.
The purpose of this paper is to investigate the integration of these previous efforts in the design of an asynchronous Bysantine- resilient computing system. The ultimate goal is a formlally verified gate-level implementation.
94. A State-Based Approach to Noninterference, William R. Bevier, William D. Young. February 1994. 19 pages.
In this report we outline an alternative approach to modeling noninterference-style security policies using a state-based model (as opposed to an event-based or i/o-based model). We argue that this approach provides a richer, more intuitive formalism for security modeling than the event-based approach and provides a link to other current research in specification and verification of concurrent and distributed systems.
93. Verifying a Simple Real-Time System with Nqthm, William D. Young. September 1993, 40 pages.
We address the formal specification and verification of a simple train crossing gate system using the Nqthm logic and automated proof system of Boyer and Moore. This problem has been suggested as a benchmark for evaluating the performance of specification tools and automated reasoning systems in the area of safety-critical systems. The system specification is presented and the proof of safety and em utility properties is outlined. The performance of Nqthm on this problem is evaluated.
92. Automated Proofs of Object Code for a Widely Used Microprocessor, Yuan Yu. December 1992. Vol. I 114 pages. Vol. II 619 pages. (There is $60.00 charge on Vol. II.)
This paper is about formally specifying and mechanically proving the correctness of machine code programs using the automated reasoning system Nqthm, also known as the Boyer-Moore Theorem Proving System. On top of Nqthm, we formally defined a mathematical model of the MC68020, a widely used microprocessor built by Motorola, at the instruction set level.
91. A Fuzzy Controller: Theorems and Proofs about its Dynamic Behavior, Miren Carranza, Bill Young. May 1993. 31 pages.
We introduce the application of formal methods techniques to verify correctness of fuzzy rule-based control systems. To this end, we have modeled a simple controller in the computational logic of Boyer and Moore and proved some theorems about its behavior using the automatic theorem prover that supports that logic. The prover incorporates execution capabilities and induction. The execution capabilities permit us to run simulations of our system. This helps us formulate conjectures about the behavior of the system. The inductive capability lets us prove our conjectures (if in fact they are theorems) for n simulation clock ticks. Our controller is a forward feeding controller which simplifies the simulation of its behavior and lets us concentrate on the verification issues related to fuzzy rule-based systems.
We also introduce two other controllers that do not satisfy the properties that our original controller was proved to satisfy. The point of this part of the exercise is to illustrate the potential of our verification technology in formally comparing different fuzzy controllers.
89. A Mathematical Model of the Mach Kernel: Atomic Actions and Locks, William Bevier, Larry Smith. April 1993. 21 pages.
This report discusses the identification and use of Mach kernel atomic actions. Mach kernel calls may be programmed as compositions of these fine-grained steps. An atomic action has well-defined output properties, so a kernel call that is programmed as a sequence of atomic actions has predictable intermediate states. This is important for dealing with such issues as error recovery, pre-emption of kernel calls, security, kernel state testing, and reasoning about the concurrent execution of kernel calls. We also discuss an important related subject: the meaning of locks.
88. A Mathematical Model of the Mach Kernel: Entities and Relations, William Bevier, Larry Smith. April 1993. 56 pages.
Mach is an operating system kernel that has been under development for a number of years, primarily at Carnegie-Mellon University. It is not a fully functional operating system. It implements a few basic abstractions like task, thread, message and port. Usable operating systems are built on top of the Mach kernel in terms of these abstractions.
This is the first in a series of reports that give a mathematical model of the functional behavior of the Mach kernel version 3.0. We have several goals in doing this work. The first is simply to provide mathematically precise documentation.
86. The FM9001 Microprocessor Proof, Bishop C. Brock, Warren A. Hunt, Jr., Matt Kaufmann. December, 1994. 1410 pages.
The FM9001 is a 32-bit, general-purpose microprocessor whose specification and netlist-level implementation have been formally described in the Nqthm logic. The FM9001 netlist has been mechanically checked to implement its specification with the Nqthm theorem-proving program. This report includes the entire formalized input: specification, implementation, and theorems, all of which have been checked with Nqthm. The FM9001 microprocessor has been fabricated as a CMOS gate array by LSI Logic, Inc. We have been testing the fabricated FM9001 for over two years and we have not yet discovered any flaws. Also included in this report is the netlist from which LSI Logic fabricated the FM9001. This report is intended to permit an Nqthm user to completely redo the FM9001 proof, and also to formalize and verify other hardware in the DUAL-EVAL hardware description language.
85. An Assistant for Reading Nqthm Proof Output, Matthew Kaufmann. November, 1992. 21 pages.
Inspection of the output of failed proof attempts is crucial to the successful use of the Boyer-Moore theorem prover. We introduce a utility that assists with the navigation of the prover's output in an Emacs environment. This utility should be a major help to beginning users of the Boyer-Moore prover, and should also be a timesaver for more advanced users.
84. Introduction to the OBDD Algorithm for the ATP Community, J Strother Moore. October, 1992. 7 pages.
We describe in terms familiar to the automated reasoning community the graph-based algorithm for deciding propositional equivalence published by R. E. Bryant in 1986. Such algorithm, based on ordered binary decision diagrams or OBDDs, are currently the fastest known ways to decide whether two propositional expressions are equivalent and are generally hundreds or thousands of times faster on such problems than most automatic theorem proving systems.
83. A Verified Implementation of an Applicative Language with Dynamic Storage Allocation, Arthur Flatau. November, 1992.
In this paper we describe a compiler for a subset of the Nqthm logic and a mechanically checked proof of its correctness. The Nqthm logic defines an applicative programming language very similar to McCarthy's pure Lisp. The compiler complies programs in the Nqthm logic into the Piton assembly level language. The correctness of the compiler is proven by showing that the result of executing the Piton code is the same as produced by the Nqthm interpreter V&C$.
82. Verifying a Knowledge-Based Fuzzy Controller, Miren Carranza. September, 1992. 24 pages.
The field of formal methods attempts to achieve system reliability by applying logic-based mathematical modeling in the construction of digital systems. In this paper we are attempting to apply such techniques to a new application domain, namely the correctness of fuzzy rule-based control systems. To this end, we have modeled a simple controller in the computationl logic of Boyer and Moore and proved some theorems about its behavior using the automatic theorem prover that supports that logic.
81. Quantification in Nqthm: a Recognizer and Some Constructive Implementations, Matthew Kaufmann. August, 1992. 24 pages.
We present an implementation of a recognizer for quantified notions in the Boyer-Moore Theorem Prover, Nqthm. That is, we provide a method for checking that a given function does indeed represent a quantified notion. We also present methods for generating constructively-presented functions that represent quantified notions, including definitions using only bounded quantifiers.
79. A Formal HDL and its use in the FM9001 Verification, Warren A. Hunt, Jr., and Bishop C. Brock. July, 1992. 17 pages.
A synchronous, hierarchical, occurrence-oriented, hardware description language (HDL) has been formalized with the Boyer-Moore logic. Well-formed HDL circuits are recognized by a predicate, and a unit-clock simulator defines the meaning of circuits expressed in the HDL. This HDL has been used to specify an implementation of the FM9001 microprocessor that has been mechanically proved to implement the FM 9001 instruction-level specification.
78. A Proved Application with Simple Real-Time Properties, Matthew Wilding. October, 1992. 108 pages
This report describes the proof of an application on the CLI short stack. The application generates moves in a game of Nim. We describe Nim and formalize the notion of optimal play. We develop a specification that also includes some simple real-time constraints. A Piton program that implements the specification is presented, along with an Nqthm-checked correctness proof. We make some observations about proving Piton programs correct, and describe the use of the fabricated FM9001 to run the compliled program.
77. Verifying the Interactive Convergence Clock Synchronization Algorithm Using the Boyer-Moore, William D. Young. April, 1992. 43 pages.
The application of formal methods to the analysis of computing systems promises to provide higher and higher levels of assurance as the sophistication of our tools and techniques increases. Improvements in tools and techniques come about as we pit the current state of the art against new and challenging problems. A promising area for the application of formal methods is in real-time and distributed computing. Some of the algorithms in this area are both subtle and important. In response to this challenge and as part of an ongoing attempt to verify an implementation of the Interactive Convergence Clock Synchronization Algorithm, we decided to undertake a proof of the correctness of the algorithm using the Boyer-Moore theorem prover. This paper describes our approach to proving the ICCSA using the Boyer-Moore prover.
76. An Introduction to a Formally Defined Hardware Description Language by Bishop C. Brock, Warren A. Hunt Jr., and William D. Young. April, 1992. 37 pages
We describe a hierarchical, occurrence-oriented hardware description language embedded within the Boyer-Moore logic. Within this formalism, we represent combinational and sequential circuits as list constants. An interpreter has been defined that gives meaning to circuit constants recognized by a well-formedness circuit predicate. Circuits can be verified with respect to their interpretations and we can write programs that manipulate HDL expressions. Instead of attempting to verify each circuit constant of interest, we often verify functions that synthesize circuit constants.
75. Response to FM 91 Survey of Formal Methods: Nqthm and Pc-Nqthm by Matt Kaufmann (with many contributors). March, 1992. 32 pages.
This report contains contributions to the requested survey for FM91, ``A survey of formal methods tools and techniques'' and ``A survey of applications.'' Two tools are covered: (1) Nqthm, the Boyer-Moore Theorem Prover; and (2) Pc-Nqthm, an interactive enhancement of Nqthm. Some of the words are taken from corresponding responses for FM89, but changes have been made.
74. A Compiler of NQTHM: A Progress Report by Arthur Flatau. January, 1992. 37 pages.
This report describes a compiler for the NQTHM logic and a mechanically checked proof of its correctness. The NQTHM logic defines an applicative programming language very similar to McCarthy's pure Lisp. The compiler compiles programs in the NQTHM logic into the Piton assembly level language. The correctness of the compiler is proven by showing that the result of executing the Piton code is the same as produced by the NQTHM interpreter v&c$. A completed prototype for the compiler is discussed.
73. The Role of Automated Reasoning in Integrated System Verification Environments by Don Good, Matt Kaufmann and J Moore. January 1992. 22 pages.
This paper focuses on ``system verification,'' the activity of mechanically proving properties of computer systems. Distinguishing characteristics of systems include their large size, their multiple layers of abstraction, and their frequent concern with multiple programming languages and, more generally, multiple models of computation. System verification systems require supreme integration of their component parts. To reason formally about systems one must be able to reason about the relations between its disparate modules, layers of abstraction, and various models of computation. Facilitating system verification is, we believe, the underlying theme of this ``Workshop on the Effective Use of Automated Reasoning Technology in System Development.'' We address that theme explicitly in this paper. We make an important, often overlooked, but essentially trivial point: to reason formally about the relations between various ideas, those ideas must be formalized. However, the popular approach to imposing formal semantics on computational models, namely the creation of ``formula generators,'' fails to formalize the very ideas allegedly being studied. In our view, this explains why so much work on system verification is thwarted by ``integration problems.'' These ``integration problems'' simply disappear when the ideas being studied are formalized and available for logical manipulation by the automated reasoning system. Our observations are supported by our experience in verifying several of the largest systems studied to date.
72. POSITION PAPER: Should We Begin a Standardization Process for Interface Logics? by Matt Kaufmann and J Moore. January 1991. 11 pages.
This paper is a companion paper to CLI Technical Report 73. In that paper we argue against so-called interface logics for the verification of systems, and present an alternative approach that has already enjoyed considerable success. In this document we raise concerns about the use of interface logics even for the verification of software or hardware whose scale is smaller than what one might normally call ``systems.''
71. Mechanically Verifying Concurrent Programs by David M. Goldschlag. September, 1991.
This thesis develops a sound, mechanically verified proof system suitable for the mechanical verification of both the safety and liveness properties of concurrent programs. Mechanical verification increases the trustworthiness of a proof. The properties proved may be (non-existentially quantified) first order, and the programs may be parameterized. The proof system provides a mechanized framework for reasoning about concurrent programs under a variety of fairness assumptions. It is demonstrated by the mechanically verified proofs of four concurrent programs. This thesis presents several significant results, including the first extensive mechanized use of proof rules which are theorems of an operational semantics.
70. Verifiable Computer Security and Hardware: Issues by William D. Young. September 1991. 43 pages. This report explores the influences of hardware on verifiable secure system design and envisions a mutually beneficial collaboration between the hardware verification and security communities. Hardware verification techniques offer the possibility of significantly enhanced assurance for secure systems at the lowest levels of system design and implementation. Security can provide an important and challenging applications arena in which hardware- oriented formal approaches can be tried and refined. We discuss some of the important concepts and issues that arise in trying to apply formal techniques to secure systems at the hardware level: the meaning of ``security'' in the context of hardware; the way to identify appropriate security properties at each level of system description, including the hardware level; and, a number of specific concerns related to hardware and its use in secure system development.
69. Mechanically Verified Hardware Implementing an 8-Bit Parallel IO Byzantine Agreement Processor by J Strother Moore. August, 1991. 37 pages.
Consider a network of four processors that use the Oral Messages (Byzantine Generals) algorithm of Pease, Shostak and Lamport to achieve agreement in the presence of faults. Bevier and Young have published a functional description of a single processor that, when interconnected appropriately with three identical others, implements this network under the assumption that the four processors step in synchrony. By formalizing the original Pease, Shostak and Lamport work, Bevier and Young mechanically proved that such a network achieves fault tolerance. In this paper we develop, formalize and discuss a hardware design that has been mechanically proved to implement their processor. In particular, we formally define mapping functions from the abstract state space of the Bevier-Young processor to a concrete state space of a hardware module and state a theorem that expresses the claim that the hardware correctly implements the processor.
68. A Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol by J Strother Moore. August, 1991. 50 pages.
In this paper we present a formal model of asynchronous communication as a function in the Boyer-Moore logic. The function transforms the signal stream generated by one processor into the signal stream consumed by an independently clocked processor. This transformation ``blurs'' edges and ``dilates'' time due to differences in the phases and rates of the two clocks and the communications delay. The model can be used quantitatively to derive concrete performance bounds on asynchronous communications at ISO protocol level 1 (physical level). We develop part of the reusable formal theory that permits the convenient application of the model. We use the theory to show that a biphase mark protocol can be used to send messages of arbitrary length between two asynchronous processors. We study two versions of the protocol, a conventional one which uses cells of size 32 cycles and an unconventional one which uses cells of size 18.
67. Mathematical Methods for Digital Systems Development by Donald I. Good and William D. Young. August 1991. 22 pages.
We explore the role of mathematical modeling in digital systems development as a way to gain enhanced assurance in their correctness. We concentrate on systems verification--the ``layering'' of verified components to construct highly reliable hierarchically-structured computing systems. We illustrate with an existing hierarchically verified system, the CLI stack, comprising a compiler for a simple high-level language, an assembler and link-loader for an assembly level language, a microprocessor with its gate level realization, and a simple multi-tasking operating system.
66. Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits, by David M. Goldschlag. March, 1991. 12 pages.
This paper describes, by means of an example, how one may mechanically verify delay insensitive circuits on an automated theorem prover. It presents the verification of both the safety and liveness properties of an n-node delay insensitive fifo circuit.
This paper describes the circuit formally in the Boyer-Moore logic and presents the mechanically verified correctness theorems. The formal description also captures the protocol that the circuit expects its environment to obey and specifies a class of suitable initial states.
65. A Mechanical Formalization of Several Fairness Notions, by David M. Goldschlag. March, 1991. 20 pages.
Fairness abstractions are useful for reasoning about computations of non-deterministic programs. This paper presents proof rules for reasoning about three fairness notions and one safety assumption with an automated theorem prover. These proof rules have been integrated into a mechanization of the Unity logic, and are suitable for the mechanical verification of concurrent programs. Mechanical verification provides greater trust in the correctness of a proof.
The three fairness notions presented here are unconditional, weak, and strong fairness. The safety assumption is deadlock freedom which guarantees that no deadlock occurs during the computation. These abstractions are demonstrated by the mechanically verified proof of a dining philosopher's program, also discussed here.
64. The AVA Reference Manual: Derived from ANSI/MIL-STD-1815A-1983, modifications by Michael K. Smith. June, 1990. 217 pages.
AVA (A Verifiable Ada) is an attempt to formally define a subset of the Ada programming language sufficient for reasonable size programming projects. Such a formal definition is a prerequisite to the production of provably correct Ada programs. This document in general is a subset of [DoD 83a] and represents the informal description of AVA. In some places we have deleted text in order to remove certain constructs from the language. In some places we have modified or added text for clarification or to state stronger restrictions than Ada.
62. Machine Checked Proofs of Byzantine Agreement Algorithm, by William Bevier and William D. Young. August, 1990. 37 pages.
We described a formally verified implementation of the Oral Messages algorithm of Pease, Shostak, and Lamport. An abstract implementation of the algorithm is verified to achieve interactive consistency in the presence of faults. This abstract characterization is then mapped down to a hardware level implementation which inherits the fault-tolerant characteristics of the abstract version. All steps in the proof were checked with the Boyer-Moore theorem prover. A significant result of this work is the demonstration of a fault-tolerant device that is formally specified and whose implementation is proved correct with respect to this specification. A significant simplifying assumption is that the redundant processors behave synchronously. We also described a mechanically checked proof that the Oral Messages algorithm is optimal in the sense that no algorithm which achieves agreement via similar message passing can tolerate a larger proportion of faulty processors.
60. A Formal Introduction to a Simple HDL, by Warren A. Hunt, Jr. and Bishop Brock. July 31, 1990. 43 pages.
A hierarchical, occurrence-oriented, combinational hardware description language has been formalized. Instead of using logic formulas to represent circuits, we represent circuits as list constants. Using a formal logic, interpreters have been defined which give meanings to circuit constants, and a good-circuit predicate recognizes well-formed circuit descriptions. We can directly verify circuit specifications, but instead we often verify functions which generate circuit constants.
59. Middle Gypsy 2.05 Definition, by Donald I. Good and Ann Siebert. May, 1990. 319 pages.
This report contains the mathematical definition of the Middle Gypsy 2.05 language. Gypsy 2.05 is a language for describing computer programs. Middle Gypsy is a slightly modified subset of Gypsy 2.05. The subset excludes concurrency and type abstraction.
58. The Boyer-Moore Prover and Nuprl: An Experimental Comparison, by Matt Kaufmann. July, 1990. 29 pages.
We use an example to compare the Boyer-Moore Theorem Prover and the Nuprl Proof Development System. The respective machine verifications of a version of Ramsey's theorem illustrate similarities and differences between the two systems. The proofs are compared using both quantitative and non-quantitative measures, and we examine difficulties in making such comparisons.
57. The Proof of Correctness of a Fault-Tolerant Circuit Design, by William Bevier and William D. Young. August, 1990. 15 pages.
We describe a formally verified implementation of the ``Oral Messages'' algorithm of Pease, Shostak, and Lamport. An abstract implementation of the algorithm has been verified to achieve interactive consistency in the presence of faults. This abstract characterization is then mapped down to a hardware level implementation which inherits the fault-tolerant characteristics of the abstract version. The proof that the hardware level description is a correct implementation of the ``Oral Messages'' algorithm has been fully checked with a mechanical theorem prover. A significant result of this work is the demonstration of a fault-tolerant device that is formally specified and whose implementation is proved correct with respect to this specification.
56. A Mechanically-Checked Correctness Proof of a Floating-Point Search Program (Draft), by Matthew Wilding. May, 1990. 72 pages.
This paper describes work toward the mechanical certification of floating-point program correctness theorem proofs. A library of useful facts about rational numbers was constructed. A set of axioms about floating-point operations has been proved consistent using a mechanical theorem prover that employs the rational number library. A small floating point program has been developed and a mechanically-checked correctness theorem about it constructed.
54. A Theorem Prover for a Computational Logic, by Robert S. Boyer and J Strother Moore. April, 1990. 17 pages.
We briefly review a mechanical theorem-prover for a logic of recursive functions over finitely generated objects including the integers, ordered pairs and symbols. The prover, known both as NQTHM and as the Boyer-Moore prover, contains a mechanized principle of induction and implementations of linear resolution, rewriting, and arithmetic decision procedures. We describe some applications of the prove including a proof of the correct implementation of a higher level language on a microprocessor defined at the gate level. We also describe the ongoing project of recoding the entire prover as an applicative function within its own logic.
53. Generalization in the Presence of Free Variables: a Mechanically- Checked Correctness Proof for One Algorithm, by Matt Kaufmann. April, 1990. 93 pages.
In this paper we present a mechanically-checked proof of correctness for a generalization algorithm. Although the theorem itself is probably new (at least, we are unaware of any existing statement of it), the interest here lies no particularly in the theorem per se but, rather, lies in the demonstration of the use of mechanical verification for assisting in the reliability of detailed proofs and software. In particular, we believe that this exercise strongly suggests the feasibility of creating a verified version of PC-NQTHM, i.e. one which is proved correct in the Boyer-Moore theorem prover or in some successor of that system. A final version of this paper has appeared in the Journal of Automated Reasoning Vol. 7, 1991, pp. 109-158.
52. The Formalization of a Simple Hardware Description Language, by Bishop C. Brock and Warren A. Hunt, Jr. November, 1989.
A hierarchical, occurrence-oriented, combinational hardware description language has been formalized using the Boyer-Moore logic. Instead of representing circuits as formulas of a particular logic, combinational circuits are represented by list constants in the Boyer-Moore logic. A good-circuit predicate recognizes well-formed circuit descriptions; an interpreter provides the semantics of the language. This approach allows the direct verification of circuit specifications, as well as allowing the verification of circuit generating functions. A circuit generating function for a family of ALUs has been verified using these techniques.
51. The Partial Specification of Microprocessor Instruction Set Architectures, by William Bevier. November, 1989.
This paper is to formally specify an instruction set architecture in a way that avoids over-specification. We wish our specification to permit reasonable implementation alternatives. For instance, our instruction set specification does not require a particular instruction format. Relaxation of requirements extends to machine size. We do not require a particular register file length, for example. The result is a specification method not for a single-architecture, but for a class of instruction set architectures.
50. The Verification of a Minimum Spanning Tree Algorithm, by David Goldschlag. October, 1989.
This paper describes a proof system suitable for the mechanical verification of concurrent programs. Mechanical verification, which uses a computer program to validate a formal proof, greatly increases one's confidence in the correctness of the validated proof. If one can assume the correctness of the proof, then one need only read, understand, and accept the specification in order to trust the coded program.
49. The Verification of a Bit-slice ALU Warren A. Hunt, Jr. and Bishop C. Brock. September, 1989. 23 pages.
The verification of a bit-slice ALU has been accomplished using a mechanical theorem prover. This ALU has an n-bit design specification, which has been verified to implement its top-level specification. The ALU and top-level specifications were written in the Boyer-Moore logic. The verification was carried out with the aid of Boyer-Moore theorem prover in a hierarchical fashion.
48. Microprocessor Design Verification, Warren A. Hunt, Jr. September, 1989. 33 pages.
The verification of a microprocessor design has been accomplished using a mechanical theorem prover. This microprocessor, the FM8502, is a 32-bit general-purpose, von Neumann processor whose design-level (gate-level) specification has been verified with respect to its instruction-level specification. Both specifications were written in the Boyer-Moore logic, and the proof of correctness was carried out with the Boyer-Moore theorem prover.
47. Mathematical Forecasting, Donald I. Good. September, 1989. 26 pages.
In aerospace and in many other fields of engineering, it is common practice to forecast the behavior of a physical system for analyzing a mathematical model of it. If the model is accurate and the analysis is mathematically sound, forecasting from the model enables an engineer to preview the effect of a design on the physical behavior of the product.
Although digital computers now are embedded as operational components in many aerospace and other physical systems, capabilities for mathematically forecasting the physical behavior of computer programs are only now beginning to emerge. Present forecasting capabilities for computer programs still are limited, but they are expanding; and even the present, limited capabilities can be useful to a practicing software engineer.
46. Report on the Formal Specification and Partial Verification of the VIPER Microprocessor, Bishop Brock and Warren A. Hunt, Jr. June 27, 1989. 26 pages.
VIPER (Verifiable Integrated Processor for Enhanced Reliability) is a 32-bit microprocessor architecture designed by the Royal Signals and Radar Establishment (RSRE) in Malvern, England. Recent technical and marketing literature describes VIPER as the first commercially available microprocessor whose gate-level design has been formally verified to meet high level specifications. The purpose of this report is to examine the claim that the gate-level design of the VIPER microprocessor is mathematically verified.
45. Comparing Specification Paradigms: Gypsy and Z, William D. Young. June, 1989. 21 pages.
We present a comparison of the Gypsy and Z specification languages in the context of a nontrivial example. Our example is a previous specification of a subset of the Unix file system functionality in Z and the translation of this specification into Gypsy. We compare and contrast the two specifications. On the basis of this comparison, certain conclusions are drawn which we hope can suggest refinements to the two languages and possibly a direction for future language designs which will avoid the pitfalls and capitalize on the strong points of each.
44. Functional Instantiation in First Order Logic (Draft), Robert S. Boyer, David Goldschlag, Matt Kaufmann and J Strother Moore. May, 1989.
43. DEFN-SK: An Extension of the Boyer-Moore Theorem Prover to Handle First-Order Quantifiers (Draft), Matt Kaufmann. May, 1989. 63 pages.
The DEFN-SK event is simply an interface from first-order logic into the Boyer-Moore logic. It introduces a new function symbol which abbreviates a first-order formula. A paper will appear in the JAR.
42. Addition of Free Variables to an Interactive Enhancement of the Boyer-Moore Theorem Prover, Matt Kaufmann. May, 1989. 15 pages.
This report is a companion to CLI Technical Report 19, which is a User's Manual for pc-nqthm, an interactive enhancement to the Boyer-Moore Theorem Prover.
41. An Approach to Systems Verification, William R. Bevier, Warren A. Hunt, Jr., J Strother Moore and William D. Young. April, 1989. 19 pages.
This paper outlines an approach to systems verification, and summarizes the application of this approach to several systems components. These components consist of a code generator for a simple high-level language (Micro Gypsy), an assembler and linking loader (Piton), a simple operating system kernel (Kit), and a microprocessor design (FM8502).
40. A Simple but Effective Incremental Development Manager (Draft), Robert L. Akers and Lawrence Smith.
This paper presents a mechanism which a software development environment may use to help maintain consistency among the various parts of a developing or evolving software system. Our view of the development process considers that (1) the program is represented as a collection of structured objects in a database and (2) the program development environment manages a collection of independent tools that operate on the database objects, storing their results in the same database.
39. A Parallel Version of the Boyer-Moore Prover, Matt Kaufmann and Matthew Wilding. February, 1989. 41 pages.
This system lets one use idle processors to increase the speed of the Boyer-Moore prover on batch jobs. It also lets one do coarse-granularity parallel processing of other jobs, such as compilation.
37. A Mechanically Verified Code Generator, William D. Young. January, 1989. 36 pages.
In this paper we describe the implementation and proof of a code generator, a major component of a compiler. The source language is a subset of Gypsy (version 2.05) and the target language is the Piton assembly level language. Our code generator is one level of a stack of verified system components including an assembler and linking loader for Piton and a microprocessor design verified at the register transfer level. This is a short description of the same work described in CLInc Report #33.
36. Mechanical Proofs about Computer Programs, Donald I. Good. March 1, 1984. 26 pages. (Unrevised edition of Technical Report 41, Institute for Computing Science and Computer Applications, The University of Texas at Austin).
The Gypsy verification environment is a large computer program that supports the development of software systems and formal, mathematical proofs about their behavior. The environment provides conventional development tools, such as a parser for the Gypsy language, an editor and compiler.
35. Report on Middle-Gypsy (Draft), Donald I. Good, Robert L. Akers, Lawrence M. Smith and William D. Young. November, 1988. 67 pages.
Gypsy is a collection of methods, languages, and tools for building formally verified computing systems. Gypsy provides capabilities for specifying a system, implementing it, and for using formal, logical deduction to prove important properties about the specification and the implementation of the system. Micro-Gypsy is a subset of Gypsy 2.05 selected as a target for a verified language implementation. It contains a large part of the executable fragment and almost all of the specification component of Gypsy 2.05. The subset described in this report is a significant extension of the Micro-Gypsy subset characterized in abstract prefix syntax in CLInc Report #33. This document has been generated by editing the Report on Gypsy 2.05 to reflect the Middle-Gypsy subset.
34. Report on Micro-Gypsy (Draft), Donald I. Good, Robert L. Akers, Lawrence M. Smith and William D. Young. November, 1988. 52 pages.
Gypsy is a collection of methods, languages, and tools for building formally verified computing systems. Gypsy provides capabilities for specifying a system, implementing it, and for using formal, logical deduction to prove important properties about the specification and the implementation of the system. Micro-Gypsy is a subset of Gypsy 2.05 selected as a target for a verified language implementation. It is a fairly restricted component of Gypsy. It does not contain abstract data types, concurrency, dynamic type, the case statement, or the rational data type. The procedural aspects of Micro-Gypsy comprise approximately the fragment of Gypsy characterized in abstract prefix syntax in CLInc Report #33. This document has been generated by editing Report on Gypsy 2.05 to reflect the Micro-Gypsy subset.
33. A Verified Code Generator for a Subset of Gypsy, William D. Young. October, 1988. 175 pages.
This report describes the specification and mechanical proof of a code generator for a subset of Gypsy 2.05 called Micro-Gypsy. Micro-Gypsy is a high-level language containing many of the Gypsy control structures, simple data types and arrays, and predefined and user-defined procedure definitions including recursive procedure definitions.
32. A Mechanically Verified Proof System for Concurrent Programs, David Goldschlag. January, 1989. 22 pages.
This report describes a mechanically verified proof system for concurrent programs. The proof system is based on Parallel Program Design: A Foundation, by K. Mani Chandy and Jayadev Misra, but is defined with respect to an operational semantics of the transition system model of concurrency. All proof rules are justified by this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the logic. The proof system has been implemented on the Boyer-Moore prover.
31. The Ford Aerospace Corporation Trusted File Server, Composite Report, John McHugh, Craig D. Singer, Bret A. Hartman and Millard C. Taylor. August, 1988. 86 pages.
This report is a composite of five internal notes produced during CLI's work on the Ford Aerospace Corp. Trusted File Server IR&D project between October of 1987 and August of 1988. Each of the individual reports comprises a chapter in the present document.
30. A Mechanically Verified Language Implementation, J Strother Moore. September, 1988. 25 pages.
This paper briefly describes a programming language, its implementation on a microprocessor via a compiler and link- assembler, and the mechanically checked proof of the correctness of the implementation. This report is a condensed version of PITON: A Verified Assembly Level Language, CLInc Report #22.
28. Kit: A Study in Operating System Verification, William R. Bevier. August, 1988. 27 pages.
The purpose of the Kit project is to address the problem of verifying a process isolation property for a multi-tasking operating system. Kit is a small operating system kernel written for a uni-processor computer with a simple von Neumann architecture. This report is a condensed version of A Verified Operating System Kernel, CLInc Report #11.
25. Basic Events for A Computational Logic, Robert S. Boyer and J Strother Moore. June, 1988. 416 pages.
This report provides the set of definitions, theorems, and other theorem-prover commands comprising the file basic.events as described in A Computational Logic Handbook, by Robert S. Boyer and J Strother Moore, Academic Press, 1988.
24. The Code for A Computational Logic, Robert S. Boyer and J Strother Moore. June, 1988. 515 pages.
This report contains the Common Lisp source code for the Boyer-Moore theorem prover, the program described in the book, A Computational Logic Handbook, by Robert S. Boyer and J Strother Moore, Academic Press, 1988. Each chapter comprises one of the source files.
22. PITON: A Verified Assembly Level Language, J Strother Moore. September, 1988. 199 pages.
This report describes a programming language, its implementation on a microprocessor via a compiler, an assembler, and a linker, and the mechanically checked proof of the correctness of the implementation. The programming language, called Piton, is a high-level assembly language designed for verified applications and as the target language for high-level language compilers. It provides execute-only programs, recursive subroutine call and return, stack-based parameter passing, local variables, global variables and arrays, a user-visible stack for intermediate computations, and seven abstract data types including integers, data addresses, program addresses and subroutine names.
21. The nanoAVA Definition, Michael K. Smith, Dan Craigen and Mark Saaltink. June, 1988. 102 pages.
This document comprises a complete description (formal and informal) of the nanoAVA subset of Ada. As such, it represents our first attempt at a complete formal and informal description of AVA (A Verifiable Ada). The intent of this work was twofold. First, we wanted to set a least upper bound. We wanted to be sure that we could formally specify an extremely trivial subset of Ada before embarking on a more ambitious subset. Secondly, we wanted to experiment with the technical approach to the definition and its presentation to the reader.
20. Predicting Computer Behavior, Donald I. Good. May, 1988. 14 pages.
The current practice of digital system engineering is not based on science and mathematics. As a result, computer systems in operation today exhibit unforeseen behaviors that cause loss of life, information, property and money. This paper identifies the major scientific and mathematical problems that need to be solved to advance the state of digital system engineering practice.
19. A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover, Matt Kaufmann. May, 1988. 71 pages.
This manual accompanies a system for checking the provability of terms in the Boyer-Moore logic. This system is loaded on top of the Boyer-Moore Theorem Prover and is integrated with that prover.
18. The User's Manual for A Computational Logic, Robert S. Boyer and J Strother Moore. 319 pages. Now available only through Academic Press as A Computational Logic Handbook, ISBN #0-12-122952.
This book is a user's guide to a computational logic. By a computational logic is meant a mathematical logic that is both oriented toward discussion of computation and mechanized so that proofs can be checked by computation. The computational logic discussed in this manual is that developed by Boyer and Moore. The manual contains a precise and complete description of that logic and a detailed reference guide to the associated mechanical theorem proving system. In addition, the manual includes a primer for the logic as a functional programming language, an introduction to proofs in the logic, a primer for the mechanical theorem prover, stylistic advice on how to use the logic and theorem prover effectively, and many examples.
17. The Underlying Semantics of Transition Systems, J. M. Crawford and D. M. Goldschlag. 14 pages.
This paper formalizes an operational semantics for the transition system model of concurrency and presents proof rules justified by that formalization. The operational semantics and the proof rules have been mechanically verified on an automated theorem prover, and have been used to mechanically verify the correctness of a message passing solution to the n-processor mutual exclusion problem.
16. The Formal Specification and Definition of KIT, William R. Bevier. December, 1987. 190 pages.
KIT is a verified operating system kernel. This technical report contains all the definitions and shells provided to the Boyer-Moore theorem prover in the specification and definition of KIT. The purpose of the KIT project is to address the problem of operating systems kernel verification. In particular, we are concerned with the correct implementation of processes.
11. A Verified Operating System Kernel, William R. Bevier. October, 1987. 103 pages.
We present a multi-tasking operating system kernel, called KIT, written in the machine language of a uni-processor von Neumann computer. The kernel is proved to implement, on this shared computer, a fixed number of conceptually distributed communicating processes. In addition to implementing processes, the kernel provides the following verified services: process scheduling, error handling, message passing, and an interface to asynchronous devices. The problem is stated in the Boyer-Moore logic, and the proof is mechanically checked with the Boyer-Moore theorem prover.
9. Proof Checking Metamathematics: Volume I and II, N. Shankar. April, 1987. 570 pages.
Formal proof-checking has long been recognized as an interesting application of computers. It has often been claimed that significant proofs in mathematics cannot be checked using an automatic proof-checker, and that formal proofs lack the intuitive plausibility and insight that informal proofs possess. We argue against these claims by presenting machine-checked versions of some landmark proofs in metamathematics, such as those of the tautology theorem, Goedel's incompleteness theorem, and the Church-Rosser theorem. These proofs were checked using the Boyer-Moore theorem prover.
8. Using the GVE: Examples of Proof Commands, William D. Young. June, 1987. 31 pages.
This note contains examples of the uses of the various proof commands available in the Gypsy Verification Environment. Most of these examples are taken from the proof of the sort routine described in the accompanying note, Using the GVE: The Proof of a Simple Sort Routine. This document is intended as a supplement to the notes for the introductory Gypsy class, and the ordering of the proof commands is as in those notes. Each prover command is briefly described and illustrated with an example of its use.
7. The Mechanical Verification Of Distributed Systems, J. M. Crawford and D. M. Goldschlag. July 1987. 113 pages.
This paper describes a theory for the mechanical verification of distributed systems which has been implemented on the Boyer-Moore theorem prover. The Boyer-Moore Logic, the language of the theorem prover, is a quantifier-free version of predicate calculus, with recursion. Our theory has been used to mechanically prove safety and liveness properties for a solution to the N-processor mutual exclusion problem. It defines a novel characterization of fairness and demonstrates the use of an operational semantics to derive proof rules.
6. The Mechanical Verification of a Microprocessor Design, Warren A. Hunt, Jr. 1987. 42 pages.
The mechanical verification of a microprocessor, FM8501, has been performed with the aid of a theorem-proving program. FM8501, a 16-bit, microprogrammed microprocessor, is formally specified in two ways: as an instruction interpreter and as a graph of digital hardware gates. The instruction interpreter is the specification for FM8501 -- for every possible instruction a new microprocessor state is defined. The hardware gate graph, which is obtained by expanding a set of recurrence relations, represents an implementation of FM8501. The mechanical verification of FM8501 conclusively demonstrates the correctness of the implementation with respect to the FM8501 specification. The verification demonstrates the correctness with respect to three mathematically constructed data-types: Boolean vectors, natural numbers, and integers.
5. Toward Verified Execution Environments, William R. Bevier, Warren A. Hunt, Jr. and William D. Young. February 1987. 22 pages.
Current verification technology provides tools for the verification of programs written into a high-level language. Even verified high-level programs may not satisfy their specifications when executed, due to errors in lower-level software and hardware. We discuss an attempt at eliminating this problem with the design of an execution environment consisting of a compiler, operating system, and processor, each of which has been mechanically verified.
4. "Proving Gypsy Programs", Richard M. Cohen. February 9, 1989. 94 pages.
Program verification applies formal understanding of programming language semantics to the practical problem of constructing reliable software. The programming language Gypsy and the Gypsy Verification Environment, a programming environment that supports development of programs, specifications, and proofs, represent significant steps in making the program verification technology available for practical use. The purpose of this report is to specify clearly the meaning of Gypsy programs, and the means by which they are proven. The semantics are presented in a "semi-formal" way, so that they are more accessible to the verification practitioner than would be more formal, mathematical semantics. First an operational semantics for a subset of Gypsy is presented. Then this model is extended to cover more complex features of the language. Using the execution semantics as the underlying conceptual base, we proceed to present the mechanisms used to generate verification conditions for the full Gypsy language, including data abstraction, concurrent programming, and exception handling.