Formal verification of state-machines using higher-order logic
- 7 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 204-207
- https://doi.org/10.1109/iccd.1989.63356
Abstract
A description is given of the formalization of some state-machine theory in a higher-order logic (HOL) theorem prover and the results obtained applying that theory. It is shown that by building state-machine theory in HOL, the verification of state-machines is rendered much more tractable. This is illustrated using a family of redundantly encoded serial-parallel multipliers Author(s) Loewenstein, P.N. Nat. Semicond. Corp., Santa Clara, CA, USAKeywords
This publication has 2 references indexed in Scilit:
- Reasoning about state machines in higher-order logicPublished by Springer Nature ,1990
- The denotational semantics of sequential machinesInformation Processing Letters, 1980