Localizing Errors in Counterexample with Iteratively Witness Searching. - ShengYu Shen; Ying Qin; Sikun Li (ATVA, 2004)

A fast counterexample minimization approach with refutation analysis and incremental SAT. - ShengYu Shen; Ying Qin; Sikun Li (ASP-DAC, 2005)

Minimizing Counterexample of ACTL Property. - ShengYu Shen; Ying Qin; Sikun Li (CHARME, 2005)

A Faster Counterexample Minimization Algorithm Based on Refutation Analysis. - ShengYu Shen; Ying Qin; Sikun Li (DATE, 2005)

Minimizing Counterexample with Unit Core Extraction and Incremental SAT. - ShengYu Shen; Ying Qin; Sikun Li (VMCAI, 2005)

Extracting Minimum Unsatisfiable Cores with a Greedy Genetic Algorithm. - Jianmin Zhang; Sikun Li; ShengYu Shen (Australian Conference on Artificial Intelligence, 2006)

A Heuristic Local Search Algorithm for Unsatisfiable Cores Extraction. - Jianmin Zhang; ShengYu Shen; Sikun Li (ICCSA (3), 2007)

Finding Unsatisfiable Subformulas with Stochastic Method. - Jianmin Zhang; ShengYu Shen; Sikun Li (IDEAL, 2007)

Synthesizing complementary circuits automatically. - ShengYu Shen; Jianmin Zhang; Ying Qin; Sikun Li (ICCAD, 2009)

Tracking Unsatisfiable Subformulas from Reduced Refutation Proof. - Jianmin Zhang; ShengYu Shen; Sikun Li (J. Softw., 2009)

A halting algorithm to determine the existence of decoder. - ShengYu Shen; Ying Qin; Jianmin Zhang; Sikun Li (FMCAD, 2010)

Synthesizing Complementary Circuits Automatically. - ShengYu Shen; Ying Qin; Kefei Wang; Liquan Xiao; Jianmin Zhang; Sikun Li (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2010)

Inferring assertion for complementary synthesis. - ShengYu Shen; Ying Qin; Jianmin Zhang (ICCAD, 2011)

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 (IDEAL, 2011)

Extracting minimal unsatisfiable subformulas in satisfiability modulo theories. - Jianmin Zhang; ShengYu Shen; Jun Zhang; Weixia Xu; Sikun Li (Comput. Sci. Inf. Syst., 2011)

A Halting Algorithm to Determine the Existence of the Decoder. - ShengYu Shen; Ying Qin; Liquan Xiao; Kefei Wang; Jianmin Zhang; Sikun Li (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2011)

Inferring Assertion for Complementary Synthesis. - ShengYu Shen; Ying Qin; Kefei Wang; Zhengbin Pang; Jianmin Zhang; Sikun Li (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2012)

Cloud-Oriented SAT Solver Based on Obfuscating CNF Formula. - Ying Qin; ShengYu Shen; Jingzhu Kong; Huadong Dai (APWeb Workshophs, 2014)

Structure-aware CNF obfuscation for privacy-preserving SAT solving. - Ying Qin; ShengYu Shen; Yan Jia 001 (MEMOCODE, 2014)

Complementary Synthesis for Encoder with Flow Control Mechanism. - Ying Qin; ShengYu Shen; Qingbo Wu 003; Huadong Dai; Yan Jia 001 (ACM Trans. Design Autom. Electr. Syst., 2015)