Hybrid verification integrating HOL theorem proving with MDG model checking

In this paper, we describe a hybrid tool for hardware formal verification that links the HOL (higher-order logic) theorem prover and (multiway decision graphs) model checker. Our tool supports abstract datatypes and uninterpreted function symbols available in MDG, allowing the verification of high-level specifications. The hybrid tool, HOL

• Type: Journal
• Year: 2006
• Where: MJ
• Authors: Rabeb Mizouni, Sofiène Tahar, Paul Curzon
• Keywords: Hardware Formal Verification, Hybrid Tool, MJ 2006, Model Checker