Hybrid tool integrating HOL theorem proving with MDG model checking

Rabeb Mizouni; Soene Tahar; Paul Curzon

Hybrid tool integrating HOL theorem proving with MDG model checking

Rabeb Mizouni, Soene Tahar, Paul Curzon

Electrical Engineering

Research output: Contribution to conference › Paper › peer-review

Abstract

We describe a hybrid tool for hardware formal verification that links the HOL theorem prover and the MDG (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-MDG, is based on an embedding in HOL of the grammar of the hardware modeling language, MDG-HDL, as well as an embedding of the first-order temporal logic ℒ _mdg used to express properties for the MDG model checker. Verification with the hybrid tool is faster and more tractable than using either tools separately. We hence obtain the advantages of both verification paradigms.

Original language	British English
Pages	392-395
Number of pages	4
State	Published - 2004
Event	16th International Conference on Microelectronics, ICM 2004 - Tunis, Tunisia Duration: 6 Dec 2004 → 8 Dec 2004

Conference

Conference	16th International Conference on Microelectronics, ICM 2004
Country/Territory	Tunisia
City	Tunis
Period	6/12/04 → 8/12/04

Cite this

@conference{9978b5df691641b0aa919ab1a9969828,

title = "Hybrid tool integrating HOL theorem proving with MDG model checking",

abstract = "We describe a hybrid tool for hardware formal verification that links the HOL theorem prover and the MDG (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-MDG, is based on an embedding in HOL of the grammar of the hardware modeling language, MDG-HDL, as well as an embedding of the first-order temporal logic ℒ mdg used to express properties for the MDG model checker. Verification with the hybrid tool is faster and more tractable than using either tools separately. We hence obtain the advantages of both verification paradigms.",

author = "Rabeb Mizouni and Soene Tahar and Paul Curzon",

year = "2004",

language = "British English",

pages = "392--395",

note = "16th International Conference on Microelectronics, ICM 2004 ; Conference date: 06-12-2004 Through 08-12-2004",

}

TY - CONF

T1 - Hybrid tool integrating HOL theorem proving with MDG model checking

AU - Mizouni, Rabeb

AU - Tahar, Soene

AU - Curzon, Paul

PY - 2004

Y1 - 2004

N2 - We describe a hybrid tool for hardware formal verification that links the HOL theorem prover and the MDG (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-MDG, is based on an embedding in HOL of the grammar of the hardware modeling language, MDG-HDL, as well as an embedding of the first-order temporal logic ℒ mdg used to express properties for the MDG model checker. Verification with the hybrid tool is faster and more tractable than using either tools separately. We hence obtain the advantages of both verification paradigms.

AB - We describe a hybrid tool for hardware formal verification that links the HOL theorem prover and the MDG (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-MDG, is based on an embedding in HOL of the grammar of the hardware modeling language, MDG-HDL, as well as an embedding of the first-order temporal logic ℒ mdg used to express properties for the MDG model checker. Verification with the hybrid tool is faster and more tractable than using either tools separately. We hence obtain the advantages of both verification paradigms.

UR - http://www.scopus.com/inward/record.url?scp=21644473786&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:21644473786

SP - 392

EP - 395

T2 - 16th International Conference on Microelectronics, ICM 2004

Y2 - 6 December 2004 through 8 December 2004

ER -

Hybrid tool integrating HOL theorem proving with MDG model checking

Abstract

Conference

Other files and links

Fingerprint

Cite this