Login | Register

Hybrid verification integrating HOL theorem proving with MDG model checking

Title:

Hybrid verification integrating HOL theorem proving with MDG model checking

Mizouni, Rabeb, Tahar, Sofiène and Curzon, Paul (2006) Hybrid verification integrating HOL theorem proving with MDG model checking. Microelectronics Journal, 37 (11). pp. 1200-1207. ISSN 00262692

[img]
Preview
Text (application/pdf)
MEJ-2006.pdf - Accepted Version
190kB

Official URL: http://dx.doi.org/10.1016/j.mejo.2006.07.019

Abstract

In this paper, we describe a hybrid tool for hardware formal verification that links the HOL (higher-order logic) 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 L"m"d"g 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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Mizouni, Rabeb and Tahar, Sofiène and Curzon, Paul
Journal or Publication:Microelectronics Journal
Date:2006
Digital Object Identifier (DOI):10.1016/j.mejo.2006.07.019
Keywords:higher-order logic; multiway decision graphs
ID Code:977377
Deposited By: DANIELLE DENNIE
Deposited On:14 Jun 2013 15:28
Last Modified:18 Jan 2018 17:44

References:

[1]
M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993

[2]
Ying Xu , Xiaoyu Song , Eduard Cerny, Model checking for a first-order temporal logic using multiway decision graphs, 1999

[3]
F. Corella , Z. Zhou , X. Song , M. Langevin , E. Cerny, Multiway Decision Graphs for Automated Hardware Verification, Formal Methods in System Design, v.10 n.1, p.7-46, February 1997 [doi>10.1023/A:1008663530211]

[4]
Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]

[5]
Otmane Aït Mohamed , Xiaoyu Song , Eduard Cerny, On the non-termination of MDG-based abstract state enumeration, Theoretical Computer Science, v.300 n.1-3, p.161-179, 07 May 2003 [doi>10.1016/S0304-3975(01)00345-0]

[6]
Z. Zhou , Xiaoyu Song , Sofiène Tahar , Eduard Cerny , Francisco Corella , Michel Langevin, Formal Verification of the Island Tunnel Controller Using Multiway Decision Graphs, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.233-247, November 06-08, 1996

[7]
S. Rajan , Natarajan Shankar , Mandayam K. Srivas, An Integration of Model Checking with Automated Proof Checking, Proceedings of the 7th International Conference on Computer Aided Verification, p.84-97, July 03-05, 1995

[8]
Klaus Schneider , Dirk W. Hoffmann, A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, p.255-272, September 01, 1999

[9]
M. Gordon, Combining deductive theorem proving with symbolic state enumeration, 21 Years of Hardware Formal Verification, Royal Society Workshop to mark 21 years of BCS FACS, UK, December 1998.

[10]
Ilan Beer , Shoham Ben-David , Cindy Eisner , Dana Fisman , Anna Gringauze , Yoav Rodeh, The Temporal Logic Sugar, Proceedings of the 13th International Conference on Computer Aided Verification, p.363-367, July 18-22, 2001

[11]
Melham, T., Integrating model checking and theorem proving in a reflective functional language. In: Integrated Formal Methods, Lecture Notes in Computer Science, vol. 2999. Springer, Berlin. pp. 36-39.

[12]
Mark Aagaard , Robert B. Jones , Carl-Johan H. Seger, Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, p.323-340, September 01, 1999

[13]
V. K. Pisini , S. Tahar , P. Curzon , O. Ait-Mohamed , X. Song, Formal hardware verification by integrating HOL and MDG, Proceedings of the 10th Great Lakes symposium on VLSI, p.23-28, March 02-04, 2000, Chicago, Illinois, United States [doi>10.1145/330855.330947]

[14]
I. Kort, S. Tahar, P. Curzon, Hierarchical formal verification using a hybrid tool, Software Tools for Technology Transfer, Springer, Berlin, vol. 4, No. 3, May 2003, pp. 313-322.

[15]
R. Mizouni, Linking HOL theorem proving and MDG model checking, Master's thesis, Electrical and Computer Engineering Department, Concordia University, 2003.

[16]
Z. Zhou, N. Boulerice, MDG Tools(V1.0) User's Manual. University of Montreal, Department of D'IRO, 1996.

[17]
Curzon, P., Tahar, S. and Ait-Mohamed, O., Verification of the MDG components library in HOL. In: Supplementary Proceedings of the International Conference on Theorem Proving in Higher-Order Logics, pp. 31-45.

[18]
Ying Xu , Eduard Cerny , Xiaoyu Song , Francisco Corella , Otmane Aït Mohamed, Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs, Proceedings of the 10th International Conference on Computer Aided Verification, p.219-231, June 28-July 02, 1998

[19]
Haiyan Xiong , Paul Curzon , Sofiène Tahar, Importing MDG Verification Results into HOL, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, p.293-310, September 01, 1999

[20]
Clarke, E.M., Grumberg, O. and Peled, D., Model Checking. MIT Press, Cambridge, MA.

[21]
R. Hum, H. Yip, H. Li, R. Mizouni, S. Tahar. A GUI for linking HOL to MDG, Technical Report, ECE Department, Concordia University, June 2002.
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top