The following is a list of available papers and technical reports. This list is not comprehensive.

*
This paper presents new inference fules for conditional statements and
looping constructs with pre and post evaluation side effects in their test
expressions. These inference rules allow us to reason about the security
properties of programs.
*

*
Much of the work on verifying software has been done on simple, often
artificial, languages or subsets of existing languages to avoid difficult
details. In trying to verify a secure application written in C, we have
encountered and overcome some semantically complicated uses of the
language. We present inference rules for assignment statements with pre
and post evaulation side effects and while loops with arbitrary pre
evaluation effects in the test expression.
*

*
As hardware designs grow in size and complexity, current design
methods are proving less adequate. Current methods for specification,
design, and test are typically empirical or informal, that is, they
are based on experience and argument. Formal methods
are solidly based on mathematical logic systems and
precise rules of inference. Formal methods offer a discipline which
complements current methods so designers can successfully meet the
demand for high performance systems.
*

*
Formal methods covers a broad and diverse set of techniques aimed at
improving computer correctness. This paper explains the role of
specifications and implementation models in formal methods, and
different approaches to proving their correspondence. We refer to
excellent overview papers and cite some recent successful examples of
using formal methods in hardware design.
*

*
This paper explores the tension between adding functionality to create
resilient software and minimizing functionality to make it more feasible to
formally verify software.
*

*
In goal-directed proofs, such as those used in HOL, tactics often must
operate on one or more specific assumptions. But goals often have
many assumptions. Currently there is no good way to
select or denote assumptions in HOL88. Most mechanisms are sensitive to
inconsequential changes or are difficult to use.
*

*
Denoting assumptions by filters (matching) makes it easier to
maintain large proofs and reuse pieces. But writing the filter
predicate can be time-consuming and distracting.
*

*
We describe an aid to proof building which synthesizes filter functions
from terms. Given examples of terms which should and should not be
matched, the function creates an ML predicate which can be used, for
example, with filter or FILTER_ASM_REWRITE_TAC.
*

*
Recently there has been much research in verifying pipelined
microprocessors. Even so, there has been little consensus on what form the
correctness statement should take. Put another way, what should we be
verifying about pipelined microprocessors? We believe that the
correctness statement should show that the parallel machine represented by the
pipeline behaves in the same manner as the sequential machine represented
by the instruction set semantics. In this paper, we present such a model
and examine four pipeline verifications to see how they compare.
*

*
This report discusses how the generic interpreter
theory can be used inside HOL theorem proving system
to specify and verify a microcoded microprocessor system. The theory
provides a methodical way to specify and verify computer systems.
*

*
What does it mean for an instruction pipeline to be correct? We
recently completed the specification and verification of a pipelined
microprocessor called Uinta. Our proof makes no simplifying
assumptions about data and control hazards. This paper presents the
specification, describes the verification, and discusses the effect of
pipelining on the correctness model.
*

*
Sawtooth is a processor with a 5-stage pipeline, interrupts, and
supervisory mode. This thesis describes the results from verifying
Sawtooth including the method used and what errors were found in the
design.
*

*
This paper presents techniques for specifying microprocessor
instruction set syntax and semantics in the HOL theorem proving
system. The paper describes the use of abstract representations for
operators and data, gives techniques for specifying instruction set
syntax, outlines the use of records in specifying semantic domains,
presents the creation of parameterized semantic frameworks, and shows
how all of these can be used to create a semantics for a
microprocessor instruction set. The verified microprocessor Uinta
provides examples for each of these.
*

*
Microprocessor verification has become an area of much interest. The
generic interpreter theory provides a model and methodology for the
specification and verification of microprocessors. Prior to this
model, most microprocessor correctness proofs were ad hoc, and the
formalism for one proof would be of little use for another. Recently,
we have updated the generic interpreter theory. This report is the
verification of a simple microprocessor called Tamarack using this new
model. Since Tamarack is simple, this should provide an excellent
example of how to apply the generic interpreter theory. *

*
This report details the specification and verification of Tamarack.
Sections two through six will highlight the specification, and
sections seven and eight will show how the verification was completed.
*

*
This report describes the generic interpreter theory in detail and
documents its mathematical foundations.
*

*
The research presented in this paper describes a parser for the
BOLT hardware description language in the HOL theorem proving
system. This provides a means of using the same language in the
theorem proving system and the VLSI CAD tools used in our work.
We have also built a semantic model in HOL for the signal values
used in the simulator in our CAD tool suite. We show how this
semantic model can be used for reasoning about the signal value data
types that are used in the BOLT hardware description language and
the VHDL Standard Logic Package.
*

*
Formal verification methods provide a way to prove that a circuit
structure correctly implements its specification. Low level gate and
transistor logic circuits can be verified using methods such as
symbolic simulation. Higher level circuits can be verified using
theorem--proving methods, providing a multi-leveled approach to
complex device verification. Correct modeling of many VLSI
circuits requires a signal value data type that includes some degree
of strength indeterminacy. The VHDL Standard Logic Package
includes such a signal value data type, t_wlogic, that includes
46 unique values. In this paper we provide a foundation for the
t_wlogic values and their resolution function that provides a
possible link between simulation and theorem-proving. A formalization
of the low level signal values used by design tools also facilitates
reasoning about CAD tools.
*

*
In the fall of 1992, we taught an introductory programming course to a
class of non-Computer Science majors. We followed an approach based
on formal specifications, with an informal translation to Pascal as an
implementation language. This anecdotal paper reports on our
experiences and ideas for future attempts.
*

*
Iterated structures occur frequently in hardware. This paper
describes properties required of mathematical relations that can be
implemented iteratively and demonstrates the use of these properties
on a generalized class of adders. This work provides a theoretical
basis for the correct synthesis of iterated arithmetic structures.
*

*
We present techniques for automating many of the tedious aspects of
hardware verification in a higher-order logic theorem proving
environment. We employ two complementary approaches. The first
involves intelligent tactics which incorporate many of the smaller
steps currently applied by the user. The second uses hardware
combinators to partially automate inductive proofs for iterated
hardware structures. We envision a system that captures most of this
reasoning in one tactic, SuperDuperHWTac. ideally, users
would use this tactic on a goal for proving that a hardware component
meets its specification, and get back a proof documented at a level
they would have written by hand. This paper presents preliminary work
toward SuperDuperHWTac in both the HOL and Nuprl proof
development systems.
*

*
Large proofs involve many theories which are usually built from
separate files. This note describes how the standard UNIX make
utility can be used to help manage large proofs. We provide a general
Makefile that can be used with few changes and a program for
automatically generating dependencies between HOL theories.
*

*
Abstract theories are widely used in mathematics because the provide a
convenient way to reason about classes of structures. Abstract
theories provide proofs about abstract structures which can then be
used to reason about specific instances of those structures. Abstract
theories are useful for specifying and verifying computer systems
because they provide structure and guidance in the specification and
verification processes and provide a convenient method of theorem
reuse. This report describes and documents a package for using
abstract theories in the HOL theorem proving system.
*

*
We present a state property called congruence and show how it
can be used to demonstrate commutivity of instructions in a modern
load--store architecture. Our analysis is particularly important in
pipelined microprocessors where instructions are frequently reordered
to avoid costly delays in execution caused by hazards. Our work has
significant implications to safety and security critical applications
since reordering can easily change the meaning and an instruction
sequence and current techniques are largely ad hoc. Our work is
done in a mechanical theorem prover and results in a set of
trustworthy rules for instruction reordering. The mechanization makes
it practical to analyze the entire instruction set.
*

*
This dissertation contains results that provide a methodological
approach to microprocessor verification. We present a hierarchical
decomposition strategy for specifying microprocessors. The
decomposition follows traditional abstraction levels used by
microprocessor designers. We show how the explicit representation of
these abstraction levels in the specification can lead to an order of
magnitude reduction in the number of long, difficult cases in a
microprocessor verification.
*

*
AVM-1 is a microprocessor designed at the University of California,
Davis to serve as a testbed for experiments in microprocessor
verification. This report is intended to document the HOL code that
verifies that the design of AVM-1 implements its specification. The
report begins by briefly describing the architecture and organization
of AVM-1. The organization of the proof is discussed and several
technical details relating to the execution of the proof scripts in HOL
are presented. The final section of the report contains all of the HOL
code necessary to perform the verification.
*

Reproduction of all or part of this work is permitted for educational or research use provided that this copyright notice is included in any copy.