Accessibility Tools

Breadcrumb

 
 

Hardware Verification Group Home > Research > Tools >

Integration of HOL and MDG

 

Members

  • Rabeb Mizouni
  • Skander Kort
  • Vijay K. Pisini
  • Sofiène Tahar

External Collaborators

  • Xiaoyu Song, University of Montreal
  • Haiyan Xiong and Dr. Paul Curzon., Middlesex University, UK
  • Otmane Ait-Mohamed, Nortel Networks, Ottawa

Description

The aim of this project is to integrate an interactive theorem proving system, namely HOL (Higher-Order Logic) and an automated decision diagram based tool called MDG (Multiway Decision Graphs). Linking HOL and MDG brings in the advantages of both, that is the scalability of HOL and the automation of MDG.

The tool is used to verify hierarchical designs through a hierarchical verification approach. A structural description as well as the behavioral specifications of all the sub-blocks have to be provided. In the hierarchical verification approach , theorems stating the correctness of the constituant sub-blocks are used as lemmas to verify the root block. The sub-blocks may be verified either in HOL or in MDG. In a HOL verification, the hierarchical structure of the sub-block may be exploited again. On the other hand, MDG verifications are performed automatically. When such verifications succeed, new theorems stating the correctness of the corresponding sub-blocks are created.

We also aim at developing a linkage between the MDG model checker and the HOL theorem prover. The hybrid tool is expected to be faster and more tractable because it benefits from the hierarchical verification, provided by HOL, and the automation provided by MDG.



Publications

  1. R. Mizouni, S. Tahar and P. Curzon: A Hybrid Tool Integrating HOL Theorem Proving with MDG Model Checking; Proc. IEEE International Conference on Microelectronics (ICM'04), Tunis, Tunisia, December 2004, pp. 392-395.
  2. R. Mizouni, S. tahar, and P. Curzon: A Hybrid Tool Integrating HOL Theorem Proving with MDG Model Checking; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2004. [20 pages]
  3. R. Mizouni, S. Tahar, and P. Curzon: On the Embedding of MDG Specification Languages in HOL; Proc. IEEE International Conference on Computer Systems and Applications (AICCSA'03), Tunis, Tunisia, July 2003. IEEE Computer Society Press.
  4. S. Kort, S. Tahar, and P. Curzon: Hierarchical Formal Verification Using a Hybrid Tool; International Journal on Software Tools for Technology Transfer, Vol. 4, No. 3, pp. 313-322, May 2003, Springer Verlag
  5. R. Mizouni, S. tahar, and P. Curzon: A Hybrid Tool Integrating HOL Theorem Proving with MDG Model Checking; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2004. [20 pages]
  6. Rabeb Mizouni: A Hybrid Tool for Linking HOL Theorem Proving with MDG Model Checking. M.A.Sc. Electrical Engineering December 2002 Graduation: Spring 2003.
  7. S. Kort, S. Tahar, and P. Curzon: Hierarchical Verification Using an MDG-HOL Hybrid Tool; In: T. Margaria and T. Melham (Eds.), Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science 2144, Springer Verlag, 2001, pp. 244-258. [Proc. 11th IFIP Conference on Correct Hardware Design and Verification Methods (CHARME'01), Livingston, Scotland, UK, September 2001.
  8. H. Xiong, P. Curzon, S. Tahar, and A. Blandford: Proving Existential Theorems when Importing Results from MDG to HOL; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'2001), Edinburgh, Scotland, UK, September 2001.
  9. P. Curzon and S. Tahar: Automating the Verification of Parameterized Hardware using a Hybrid Tool; Proc. IEEE 13th International Conference on Microelectronics (ICM'01), Rabat, Morocco, October 2001.
  10. H. Xiong, P. Curzon, S. Tahar, and A. Blandford: Embedding and Verification of an MDG-HDL Translator in HOL; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'2000), Portland, Oregon, USA, August 2000, pp. 237-248.
  11. S. Kort, S. Tahar, P. Curzon, X. Song: HOL-MDG: A Hybrid Tool for Formal Verification; Proc. 2000 Micronet Annual Workshop, Ottawa, Canada, April 2000, pp. 131-132.
  12. V.K. Pisini, S. Tahar, P. Curzon, O. Ait-Mohamed and X. Song: Formal Hardware Verification by Integrating HOL and MDG; Proc. IEEE 10th Great Lakes Symposium on VLSI (GLS-VLSI'00), Chicago, Illinois, USA, March 2000.
  13. Vijay Kumar Pisini. Thesis Title: Integration of HOL and MDG for Hardware Verification, Co-supervisor: Dr. X. Song (University of Montreal) Thesis Defense: February 2000.
  14. V.K. Pisini, S. Tahar, P. Curzon, O. Ait-Mohamed, and X. Song : Integration of HOL and MDG for Hardware Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, November 1999. [20 pages]
  15. H. Xiong, P. Curzon, and S. Tahar: Importing MDG Results into HOL; Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'99), Nice, France, September 1999.
  16. V.K. Pisini, S. Tahar, O. Ait-Mohamed, P. Curzon, and X. Song: An Approach to Link HOL and MDG for Hardware Verification; Proc.1999 Micronet Annual Workshop, Ottawa, Canada, April 1999, pp. 156-157.
  17. P. Curzon, S. Tahar, and O. Ait-Mohamed: Verification of the MDG Components Library in HOL; In: J. Grundy and M. Newey (Eds.), Theorem Proving in Higher Order Logics: Emerging Trends, The Australian National University, 1998, pp. 31-45.


 
 

Concordia University