Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

6

MJ
2006

favoriteEmaildiscussreport

102views more MJ 2006»

Hybrid verification integrating HOL theorem proving with MDG model checking

13 years 4 months ago

Hybrid verification integrating HOL theorem proving with MDG model checking

Download hvg.ece.concordia.ca

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

Rabeb Mizouni, Sofiène Tahar, Paul Curzon

Real-time Traffic

Hardware Formal Verification | Hybrid Tool | MJ 2006 | Model Checker |

claim paper

Related Content

» Providing Automated Verification in HOL Using MDGs

» LCFstyle for Secure Verification Platform based on Multiway Decision Graphs

» A Lightweight Integration of Theorem Proving and Model Checking for System Verification

» Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

» Embedding Imperative Synchronous Languages in Interactive Theorem Provers

» Formal verification of standards for distance vector routing protocols

» A Methodology for LargeScale Hardware Verification

» Automatic Verification of Transactions on an ObjectOriented Database

» Differential Dynamic Logics

Post Info
More Details (n/a)

Added	14 Dec 2010
Updated	14 Dec 2010
Type	Journal
Year	2006
Where	MJ
Authors	Rabeb Mizouni, Sofiène Tahar, Paul Curzon

Comments (0)