FORMAL METHODS AND VERIFICATION PAPERS.

• M. Aboulhamid, X. Song. Hardware design and verification methods. Encyclopedia of Computer and Technology, Marcel Dekker, Inc, New York, 1999.
  
  
• E. Cerny, F. Corella, M. Langevin, X. Song, S. Tahar, Z. Zhou. Automated verification with abstract state machines using multiway decision graphs. Formal Hardware Verification: Methods and Systems in Comparison, pp. 79-113, edited by T. Kropf, Springer-Verlag Publishers, 1997.
  
  
• O. Ait-Mohamed, X. Song, E. Cerny. On the non-termination of MDG-based abstract state enumeration. Advances in Hardware Design and Verification, pp. 218-235, edited by H. F. Li and D. K. Probst, Chapman & Hall, 1997.
  
  
• S. Tahar, X. Song, E. Cerny, Z. Zhou, M. Langevin. Formal verification of an ATM switch fabric using multiway decision graphs. IEEE Transactions on Computer-Aided Design, vol. 18(7), pp. 956-972, July 1999.
  
  
• F. Corella, Z. Zhou, X. Song, M. Langevin, E. Cerny. Multiway decision graphs for automated hardware verification. Formal Methods in System Design, Kluwer Academic Publishers, 10(1), pp. 7-46, 1997.
  
  
• Z. Zhou, X. Song, F. Corella, E. Cerny, M. Langevin. ``Description and verification of RTL designs using multiway decision graphs.'' Proc. of the IFIP Conference on Hardware Description Languages and Their Applications (CHDL-95), , pp. 575-580, Tokyo, Japan, 1995.
  
  
• F. Corella, M. Langevin, E. Cerny, Z. Zhou, X. Song. ``State enumeration with abstract descriptions of state machines.'' Proc. of the IFIP Conference on Correct Hardware Design and Verification Methods (CHARME'95), 15 pages, Frankfurt, Germany, 1995.
  
  
  
  
• Z. Zhou, X. Song, S. Tahar, E. Cerny, F. Corella and M. Langevin. ``Formal Verification of the Island Tunnel Controller using Multiway Decision Graphs.'' Proc. of International Conference on Formal Methods in Computer Aided Design (FMCAD'96), Lecture Notes in Computer Science 1166, pp. 233-247, Palo Alto, CA, USA, 1996.
  
  
• S. Tahar, Z. Zhou, X. Song, E. Cerny and M. Langevin. ``Verification of an ATM switch fabric using multiway decision graphs.'' Proc. 1996 Micronet Annual Workshop, pp. 77-78, Ottawa, Canada, March 1996.
  
  
• M. Langevin, S. Tahar, Z. Zhou, X. Song, E. Cerny. ``Behavioral verification of an ATM switch fabric using implicit abstract state enumeration.'' Proc. of International Conference on Computer Design (ICCD'96), pp. 20-26, Austin, TX, USA, 1996.
  
  
• Z. Zhou, X. Song, F. Corella, M. Langevin, E.Cerny, and S. Tahar. ``MDG tools for the verification of RTL designs.'' Proc. of the International Conference on Computer Aided Verification (CAV `96), Lecture Notes in Computer Science 1102, pp. 433-436, NJ, USA, 1996.
  
  
• S. Tahar, Z. Zhou, X. Song, E. Cerny, M. Langevin. ``Formal verification of an ATM switch fabric using multiway decision graphs.'' Proc. of the IEEE 6th Great Lakes Symposium on VLSI, pp. 106-111, USA, 1996.
  
  
  
  
• O. Ait-Mohamed, X. Song, E. Cerny. ``On the non-termination of MDG-based abstract state enumeration.'' Proc. of IFIP International Conference on Correct Hardware Design and Verification Methods, (CHARME'97), pp. 218-235, Montreal, Canada, 1997.
  
  
  
  
• M. Azizi, O. Ait-Mohamed, X. Song. ``Cache coherence protocol verification of multiprocessor system with shared memory.'' Proc. of The IEEE 10th International Conference on Microelectronics (ICM'98), pp. 99-102, Monastir (Tunisia), December 14-16, 1998.
  
  
• J. Lu, D. Voicu, S. Tahar, X. Song. ``Model checking for a real ATM switch,'' Proc. of the International Conference on Computer Design (ICCD'98), pp. 195-198, 1998.
  
  
• D. Voicu, E. Cerny, X. Song ``Property verification of an ATM switch port controller using model checking,'' Proc. of the 5th International Conference on Electronic Devices and Systems, 1998.
  
  
• X. Song, Y. Wang. ``On the FPGA board level routing problem,'' IEEE 1998 Canadian Conference on Electrical and Computer Engineering (CCECE'98), Waterloo, Canada, 1998.
  
  
• Y. Xu, E. Cerny, X. Song, F. Corella, O. Ait-Mohamed. Model checking for a first-order temporal logic using multiway decision graphs. Proc. of the International Conference on Computer-Aided Verification (CAV'98), Lecture Notes in Computer Science 1427, 219-231, 1998.
  
  
• O. Ait-Mohamed, E. Cerny, X. Song. ``MDGs-based Verification by Retiming and Combinational Transformations,'' Proc. of the IEEE 8th Great Lakes Symposium on VLSI, pp. 356-361, Louisiana, 1998.
  
  
• V. Pisini, Tahar, O. Ait-Mohamed, X. Song. An approach to linking MDG and HOL for hardware verification. Proc. of 1999 Micronet Annual Workshop, 156-157, Ottawa, Canada, April 1999.
  
  
• V. Pisini, Tahar, O. Ait-Mohamed, P. Curzy, X. Song. Formal Hardware Verification by integrating HOL and MDG. Proc. of the IEEE 9th Great Lakes Symposium on VLSI, 2000.
  
  
• S. Tahar, X. Song, E. Cerny, Z. Zhou, M. Langevin. ``Formal verification of an ATM switch fabric using multiway decision graphs.'' Technical Report 1101, University of Montréal, 33 pages, December 1997.
  
  
• O. Ait-Mohamed, X. Song, E. Cerny. ``On the non-termination of MDG-based abstract state enumeration.'' Technical Report 1070, University of Montréal, 20 pages, May 1997.
  
  
• Z. Zhou, X. Song, S. Tahar, E. Cerny, F. Corella and M. Langevin. ``Formal Verification of the Island Tunnel Controller using Multiway Decision Graphs.'' Technical Report 1042, University of Montréal, 20 pages, 1996.
  
  
• M. Langevin, S. Tahar, Z. Zhou, X. Song, E. Cerny. ``Behavioral verification of an ATM switch fabric using implicit abstract state enumeration.'' Technical Report 1021, University of Montréal, 14 pages, 1996.