Reachability programming in hol98 using bdds

14Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.
Get full text

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 p t t-» b meaning "logical term t is represented by BDD b with respect to variable order p". 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.

Cite

CITATION STYLE

APA

Gordon, M. J. C. (2000). Reachability programming in hol98 using bdds. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1869, pp. 179–196). Springer Verlag. https://doi.org/10.1007/3-540-44659-1_12

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free