Hol98 and ROBDDs

Hol98 has been integrated with the BuDDy BDD package. The aim is to provide a research platform for experimenting with the combination of user guided deduction and efficient automatic verification methods.

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).

Transparencies


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 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


Papers to Celebrate Tony Hoare's Work

Here is a revised draft of the paper I wrote for for the Symposium in Celebration of the work of Tony Hoare. A preliminary version was included in the Proceedings handed out to participants.

Title
Programming combinations of deduction and BDD-based 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 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.
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 ]


Documentation for HolBddLib

University of Cambridge Computer Laboratory Technical Report No. 481

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 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 state enumeration.
70 pages of postscript


MICHAEL J. C. GORDON
University of Cambridge Computer Laboratory
New Museums Site
Pembroke Street
Cambridge CB2 3QG
United Kingdom
work: (+44) 1223 334627
fax: (+44) 1223 334678
home: (+44) 1223 362123
email: mjcg@cl.cam.ac.uk