Here is a talk on some experiments done over the summer of 1998.
Title
Combining Deductive Theorem Proving with Symbolic State Enumeration
Abstract
Ken Larsen has linked the
BuDDy BDD package to Moscow ML. Using this, an extensible table
mapping Hol98 terms to BDDs is described and various combinations of
deduction and symbolic state enumeration explored. For example, (i)
deduction can improve symbolic state enumeration by simplifying terms
to avoid having to create large intermediate BDDs and (ii) BDD
algorithms can augment deduction by finding countexamples and
computing explicit symbolic representations of sets of reachable
states.
Several examples are presented, including an autopilot (previously analysed by deduction in PVS and ACL2) and an asynchronous arbiter circuit (previously analysed algorithmically with Voss).
A more general talk entitled 21 Years of Hardware Verification given at the Royal Society to mark 21 years of BCS FACS
A paper submitted to TPHOLs2000.
Title
Reachability programming in Hol98 using BDDs
Author
Mike Gordon
Abstract
Two methods of programming BDDbased symbolic algorithms in the Hol98
proof assistant are presented. The goal is to provide a platform for
implementing intimate combinations of deduction and algorithmic
verification, like model checking. The first programming method uses
a small kernel of ML functions to convert between BDDs, terms and
theorems. It is easy to use and is suitable for rapid prototying
experiments. The second method requires lowerlevel programming but
can support more efficient calculations. It is based on an LCFlike
use of an abstract type to encapsulate rules for manipulating
judgements r t > b meaning ``logical term t is
represented by BDD b with respect to variable order r''. The
two methods are illustrated by showing how to perform the standard
fixedpoint calculation of the BDD of the set of reachable states of a
finite state machine.
18 pages of postscript
Title
Programming combinations of deduction
and BDDbased symbolic calculation
Abstract
Theorem provers descended from LCF allow their users to
write complex proof tools that provide high assurance that
false theorems will not be proved. This paper describes some
experiments in extending the `LCF approach' to enable BDDbased
symbolic algorithms to be programmed with a similar
assurance. The deduction is supplied by the HOL system and the BDD
algorithms by the BuDDy package.
postscript
The slides for my 20 minute talk are available.
postscript
This paper is now a Technical Report No. 480 from the University of Cambridge Computer Laboratory.
The final version for publication needed to be at most ten pages. To achieve this I have reoriented the focus of the paper away from implementation and examples and concentrated on methodology and underlying principles. In fact, this makes the paper a better match to the talk I gave.
Title
Linking higher order logic
to binary decision diagrams
Publication
To appear in Proceedings
of the Symposium in Celebration of the work of C.A.R. Hoare
(editors Jim Davies, Jim Woodcock and Bill Roscoe),
to be published as the first volume in the series "Cornerstones
in Computing" (series editor Richard Bird), MacMillan.
[postscript

latex
]
Title
Combining the Hol98 Proof Assistant
with the BuDDy BDD package
Authors
Mike Gordon and Ken Friis Larsen
Abstract
Theorem provers descended from LCF allow their users to
write complex proof tools with high assurance that
false theorems will not be proved. This report describes
an experimental system that extends
the LCF approach to enable combinations of deduction and BDDbased
symbolic calculation to be programmed with a similar
assurance. The deduction is supplied by the Hol98 system and the BDD
algorithms by Jørn LindNielsen's BuDDy package.
The main idea is to provide LCFstyle support to a set of inference rules for judgements r t > b, where r is an orderinducing map from HOL variables to BDD variables, t is a HOL term and b is a BDD. A single oracle rule allows a HOL theorem  t to be deduced from r t > b.
This report is intended to serve as documentation
for the Hol98 library HolBddLib. It is
partly an exposition of standard results, partly tutorial and
partly an account of research in combining deduction and symbolic
state enumeration.
70 pages of postscript
MICHAEL J. C. GORDON