State enumeration with abstract descriptions of state machines. - Francisco Corella; Michel Langevin; Eduard Cerny; Zijian Zhou 001; Xiaoyu Song (CHARME, 1995)

Partitioning transition relations efficiently and automatically. - Zijian Zhou 001; Xiaoyu Song; Francisco Corella; Eduard Cerny; Michel Langevin (Great Lakes Symposium on VLSI, 1995)

MDG Tools for the Verification of RTL Designs. - K. D. Anon; N. Boulerice; Eduard Cerny; Francisco Corella; Michel Langevin; Xiaoyu Song; Sofiène Tahar; Ying Xu; Zijian Zhou 001 (CAV, 1996)

Formal Verification of the Island Tunnel Controller Using Multiway Decision Graphs. - Zijian Zhou 001; Xiaoyu Song; Sofiène Tahar; Eduard Cerny; Francisco Corella; Michel Langevin (FMCAD, 1996)

Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs. - Sofiène Tahar; Zijian Zhou 001; Xiaoyu Song; Eduard Cerny; Michel Langevin (Great Lakes Symposium on VLSI, 1996)

Behavioral Verification of an ATM Switch Fabric using Implicit Abstract State Enumeration. - Michel Langevin; Sofiène Tahar; Zijian Zhou 001; Xiaoyu Song; Eduard Cerny (ICCD, 1996)

Verification with Abstract State Machines Using MDGs. - Eduard Cerny; Francisco Corella; Michel Langevin; Xiaoyu Song; Sofiène Tahar; Zijian Zhou 001 (Formal Hardware Verification, 1997)

Multiway Decision Graphs for Automated Hardware Verification. - Francisco Corella; Zijian Zhou 001; Xiaoyu Song; Michel Langevin; Eduard Cerny (Formal Methods Syst. Des., 1997)

Modeling and formal verification of the Fairisle ATM switch fabricusing MDGs. - Sofiène Tahar; Xiaoyu Song; Eduard Cerny; Zijian Zhou 001; Michel Langevin; Otmane Aït Mohamed (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999)

MDG-Based State Enumeration By Retiming And Circuit Transformation. - Otmane Aït Mohamed; Xiaoyu Song; Eduard Cerny; Sofiène Tahar; Zijian Zhou 001 (J. Circuits Syst. Comput., 2004)