| Symbolic model checking without BDDs A Biere, A Cimatti, E Clarke, Y Zhu Tools and Algorithms for the Construction and Analysis of Systems: 5th …, 1999 | 3468 | 1999 |
| Bounded model checking A Biere Handbook of satisfiability, 739-764, 2021 | 1713 | 2021 |
| Bounded model checking using satisfiability solving E Clarke, A Biere, R Raimi, Y Zhu Formal methods in system design 19, 7-34, 2001 | 1116 | 2001 |
| Symbolic model checking using SAT procedures instead of BDDs A Biere, A Cimatti, EM Clarke, M Fujita, Y Zhu Proceedings of the 36th annual ACM/IEEE Design Automation Conference, 317-320, 1999 | 1073 | 1999 |
| Verifying safety properties of a PowerPC− microprocessor using symbolic model checking without BDDs A Biere, E Clarke, R Raimi, Y Zhu Computer Aided Verification: 11th International Conference, CAV’99 Trento …, 1999 | 224 | 1999 |
| Formal property verification by abstraction refinement with formal, simulation and hybrid engines D Wang, PH Jiang, J Kukula, Y Zhu, T Ma, R Damiano Proceedings of the 38th annual Design Automation Conference, 35-40, 2001 | 106 | 2001 |
| Ordered semantic hyper-linking DA Plaisted, Y Zhu Journal of Automated Reasoning 25 (3), 167-217, 2000 | 97 | 2000 |
| Conformational analysis of molecular chains using nano-kinematics D Manocha, Y Zhu, W Wright Bioinformatics 11 (1), 71-86, 1995 | 91 | 1995 |
| Combining symbolic model checking with uninterpreted functions for out-of-order processor verification S Berezin, A Biere, E Clarke, Y Zhu Formal Methods in Computer-Aided Design: Second International Conference …, 1998 | 84 | 1998 |
| A satisfiability procedure for quantified boolean formulae DA Plaisted, A Biere, Y Zhu Discrete Applied Mathematics 130 (2), 291-328, 2003 | 76 | 2003 |
| A fast algorithm and system for the inverse kinematics of general serial manipulators D Manocha, Y Zhu Proceedings of the 1994 IEEE international conference on robotics and …, 1994 | 61 | 1994 |
| Bounded Model Checking, volume 58 of Advances in computers A Biere, A Cimatti, EM Clarke, O Strichman, Y Zhu Academic press, 2003 | 59 | 2003 |
| Guiding SAT diagnosis with tree decompositions P Bjesse, J Kukula, R Damiano, T Stanion, Y Zhu Theory and Applications of Satisfiability Testing: 6th International …, 2004 | 48 | 2004 |
| The Efficiency of Theorem Proving Strategies DA Plaisted, Y Zhu Vieweg, 1997 | 48 | 1997 |
| Kinematic Manipulation of Molecular Chains Subject to Rigid Constraint. D Manocha, Y Zhu ISMB, 285-293, 1994 | 33 | 1994 |
| Using cutwidth to improve symbolic simulation and boolean satisfiability D Wang, E Clarke, Y Zhu, J Kukula Sixth IEEE International High-Level Design Validation and Test Workshop, 165-170, 2001 | 32 | 2001 |
| Multiple state and single state tableaux for combining local and global nodel checking A Biere, Y Zhu, EM Clarke Correct System Design: Recent Insights and Advances, 163-179, 1999 | 31 | 1999 |
| Method and apparatus for performing generator-based verification Y Zhu, JH Kukula US Patent 7,149,987, 2006 | 26 | 2006 |
| Verification of out-of-order processor designs using model checking and a light-weight completion function S Berezin, E Clarke, A Biere, Y Zhu Formal Methods in System Design 20, 159-186, 2002 | 26 | 2002 |
| Bounded Model Checking-2 Model Checking A Biere, A Cimatti, EM Clarke, O Strichman, Y Zhu Advances in Computers 58, 121-125, 2003 | 15 | 2003 |
