Analytica - A Theorem Prover in Mathematica. - Edmund M. Clarke; Xudong Zhao 005 (CADE, 1992)

Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. - Edmund M. Clarke; Xudong Zhao 005 (CADE, 1994)

Fast Spectrum Computation for Logic Functions using Binary Decision Diagrams. - Masahiro Fujita; Jerry Chih-Yuan Yang; Edmund M. Clarke; Xudong Zhao 005; Patrick C. McGeer (ISCAS, 1994)

Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. - Edmund M. Clarke; Orna Grumberg; Kenneth L. McMillan; Xudong Zhao 005 (DAC, 1995)

Hybrid decision diagrams. - Edmund M. Clarke; Masahiro Fujita; Xudong Zhao 005 (ICCAD, 1995)

Word Level Model Checking - Avoiding the Pentium FDIV Error. - Edmund M. Clarke; Manpreet Khaira; Xudong Zhao 005 (DAC, 1996)

Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking. - Yirng-An Chen; Edmund M. Clarke; Pei-Hsin Ho; Yatin Vasant Hoskote; Timothy Kam; Manpreet Khaira; John W. O'Leary; Xudong Zhao 005 (FMCAD, 1996)

Word Level Model Checking (Abstract). - Edmund M. Clarke; Xudong Zhao 005 (MFCS, 1996)

Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. - Edmund M. Clarke; Kenneth L. McMillan; Xudong Zhao 005; Masahiro Fujita; Jerry Chih-Yuan Yang (Formal Methods Syst. Des., 1997)

Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. - Andrej Bauer; Edmund M. Clarke; Xudong Zhao 005 (J. Autom. Reason., 1998)

Coverage Estimation for Symbolic Model Checking. - Yatin Vasant Hoskote; Timothy Kam; Pei-Hsin Ho; Xudong Zhao 005 (DAC, 1999)

Verifying the SRT Division Algorithm Using Theorem Proving Techniques. - Edmund M. Clarke; Steven M. German; Xudong Zhao 005 (Formal Methods Syst. Des., 1999)