Here is a talk on some experiments done over the summer of 1998.
Combining Deductive Theorem Proving with Symbolic State Enumeration
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.
Reachability programming in Hol98 using BDDs
Two methods of programming BDD-based 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 lower-level programming but can support more efficient calculations. It is based on an LCF-like 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 fixed-point calculation of the BDD of the set of reachable states of a finite state machine.
18 pages of postscript
Programming combinations of deduction and BDD-based symbolic calculation
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 BDD-based 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.
The slides for my 20 minute talk are available.
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.
Linking higher order logic to binary decision diagrams
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 ]
Combining the Hol98 Proof Assistant with the BuDDy BDD package
Mike Gordon and Ken Friis Larsen
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 BDD-based symbolic calculation to be programmed with a similar assurance. The deduction is supplied by the Hol98 system and the BDD algorithms by Jørn Lind-Nielsen's BuDDy package.
The main idea is to provide LCF-style support to a set of inference rules for judgements r  t ->  b, where r is an order-inducing 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
70 pages of postscript
MICHAEL J. C. GORDON