A Fast Algorithm and System for the Inverse Kinematics of General Serial Manipulators. - Dinesh Manocha; Yunshan Zhu (ICRA, 1994)

Kinematic Manipulation of Molecular Chains Subject to Rigid Constraint. - Dinesh Manocha; Yunshan Zhu (ISMB, 1994)

Conformational analysis of molecular chains using nano-kinematics. - Dinesh Manocha; Yunshan Zhu; William V. Wright (Comput. Appl. Biosci., 1995)

The efficiency of theorem proving strategies - a comparative and asymptotic analysis. - David A. Plaisted; Yunshan Zhu (Vieweg, 1997)

Equational Reasoning using AC Constraints. - David A. Plaisted; Yunshan Zhu (IJCAI (1), 1997)

Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. - Sergey Berezin; Armin Biere; Edmund M. Clarke; Yunshan Zhu (FMCAD, 1998)

Replacement Rules with Definition Detection. - David A. Plaisted; Yunshan Zhu (FTP (LNCS Selection), 1998)

Multiple State and Single State Tableaux for Combining Local and Global Model Checking. - Armin Biere; Edmund M. Clarke; Yunshan Zhu (Correct System Design, 1999)

Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. - Armin Biere; Edmund M. Clarke; Richard Raimi; Yunshan Zhu (CAV, 1999)

Symbolic Model Checking Using SAT Procedures instead of BDDs. - Armin Biere; Alessandro Cimatti; Edmund M. Clarke; Masahiro Fujita; Yunshan Zhu (DAC, 1999)

Symbolic Model Checking without BDDs. - Armin Biere; Alessandro Cimatti; Edmund M. Clarke; Yunshan Zhu (TACAS, 1999)

Combining Local and Global Model Checking. - Armin Biere; Edmund M. Clarke; Yunshan Zhu (SMC@FLoC, 1999)

Ordered Semantic Hyper-Linking. - David A. Plaisted; Yunshan Zhu (J. Autom. Reason., 2000)

Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines. - Dong Wang; Pei-Hsin Ho; Jiang Long; James H. Kukula; Yunshan Zhu; Hi-Keung Tony Ma; Robert F. Damiano (DAC, 2001)

Using cutwidth to improve symbolic simulation and Boolean satisfiability. - Dong Wang; Edmund M. Clarke; Yunshan Zhu; James H. Kukula (HLDVT, 2001)

Bounded Model Checking Using Satisfiability Solving. - Edmund M. Clarke; Armin Biere; Richard Raimi; Yunshan Zhu (Formal Methods Syst. Des., 2001)

Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. - Sergey Berezin; Edmund M. Clarke; Armin Biere; Yunshan Zhu (Formal Methods Syst. Des., 2002)

Generator-based Verification. - Yunshan Zhu; James H. Kukula (ICCAD, 2003)

Guiding SAT Diagnosis with Tree Decompositions. - Per Bjesse; James H. Kukula; Robert F. Damiano; Ted Stanion; Yunshan Zhu (SAT, 2003)

Bounded model checking. - Armin Biere; Alessandro Cimatti; Edmund M. Clarke; Ofer Strichman; Yunshan Zhu (Adv. Comput., 2003)

A satisfiability procedure for quantified Boolean formulae. - David A. Plaisted; Armin Biere; Yunshan Zhu (Discret. Appl. Math., 2003)

Formal model construction using HDL simulation semantics. - Joseph Buck; Dong Wang; Yunshan Zhu (HLDVT, 2007)