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.