Formal verification of state-machines using higher-order logic
Paul Loewenstein · 2003
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.>