, O. Ait-Mohamed

In order to overcome the limitations of automated tools and the cumbersome proof process of interactive theorem proving, we adopt a hybrid approach for formal hardware verication which uses the strengths of the-orem proving (HOL) with powerful mathematical tools such as induction and abstraction, and the advantages of automated tools (MDG) which support equivalence checking and model checking. The MDG system is a decision diagram based verication tool, primarily de-signed for hardware verication. HOL is a theorem prover built on higher-order logic.