| 2014 | APWEB | Cloud-Oriented SAT Solver Based on Obfuscating CNF Formula. | Ying Qin, ShengYu Shen, Jingzhu Kong, Huadong Dai |
| 2014 | MEMOCODE | Structure-aware CNF obfuscation for privacy-preserving SAT solving. | Ying Qin, ShengYu Shen, Yan Jia |
| 2011 | ICCAD | Inferring assertion for complementary synthesis. | ShengYu Shen, Ying Qin, Jianmin Zhang |
| 2011 | IDEAL | Finding First-Order Minimal Unsatisfiable Cores with a Heuristic Depth-First-Search Algorithm. | Jianmin Zhang, Weixia Xu, Jun Zhang, ShengYu Shen, Zhengbin Pang, Tiejun Li, Jun Xia, Sikun Li |
| 2010 | FMCAD | A halting algorithm to determine the existence of decoder. | ShengYu Shen, Ying Qin, Jianmin Zhang, Sikun Li |
| 2009 | ICCAD | Synthesizing complementary circuits automatically. | ShengYu Shen, Jianmin Zhang, Ying Qin, Sikun Li |
| 2007 | ICCSA | A Heuristic Local Search Algorithm for Unsatisfiable Cores Extraction. | Jianmin Zhang, ShengYu Shen, Sikun Li |
| 2007 | IDEAL | Finding Unsatisfiable Subformulas with Stochastic Method. | Jianmin Zhang, ShengYu Shen, Sikun Li |
| 2005 | ASPDAC | A fast counterexample minimization approach with refutation analysis and incremental SAT. | ShengYu Shen, Ying Qin, Sikun Li |
| 2005 | DATE | A Faster Counterexample Minimization Algorithm Based on Refutation Analysis. | ShengYu Shen, Ying Qin, Sikun Li |
| 2005 | VMCAI | Minimizing Counterexample with Unit Core Extraction and Incremental SAT. | ShengYu Shen, Ying Qin, Sikun Li |
| 2004 | ATVA | Localizing Errors in Counterexample with Iteratively Witness Searching. | ShengYu Shen, Ying Qin, Sikun Li |