SAT-Based Automata Construction for LTL over Finite Traces. - Yingying Shi; Shengping Xiao; Jianwen Li; Jian Guo 005; Geguang Pu (APSEC, 2020)

On-the-fly Synthesis for LTL over Finite Traces. - Shengping Xiao; Jianwen Li; Shufang Zhu 001; Yingying Shi; Geguang Pu; Moshe Y. Vardi (AAAI, 2021)

Combining BMC and Complementary Approximate Reachability to Accelerate Bug-Finding. - Xiaoyu Zhang; Shengping Xiao; Jianwen Li; Geguang Pu; Ofer Strichman (ICCAD, 2022)

LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work. - Giuseppe De Giacomo; Marco Favorito; Jianwen Li; Moshe Y. Vardi; Shengping Xiao; Shufang Zhu 001 (IJCAI, 2022)

Identifying Boundary Conditions with the Syntax and Semantic Information of Goals. - Yechuan Xia; Jianwen Li; Shengping Xiao; Weikai Miao; Geguang Pu (CoRR, 2022)

LTLf Satisfiability Checking via Formula Progression (S). - Tong Niu; Yicong Xu; Shengping Xiao; Lili Xiao; Yanhong Huang; Jianwen Li (SEKE, 2023)

FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format. - Shengping Xiao; Chengyu Zhang 001; Jianwen Li; Geguang Pu (TACAS (2), 2023)

Accelerate Safety Model Checking Based on Complementary Approximate Reachability. - Xiaoyu Zhang; Shengping Xiao; Yechuan Xia; Jianwen Li; Mingsong Chen 001; Geguang Pu (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2023)

Model-Guided Synthesis for LTL over Finite Traces. - Shengping Xiao; Yongkang Li; Xinyue Huang; Yicong Xu; Jianwen Li; Geguang Pu; Ofer Strichman; Moshe Y. Vardi (VMCAI (1), 2024)

On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts. - Shengping Xiao; Yongkang Li; Shufang Zhu 001; Jun Sun 001; Jianwen Li; Geguang Pu; Moshe Y. Vardi (CoRR, 2024)

Computing minimal unsatisfiable core for LTL over finite traces. - Tong Niu; Shengping Xiao; Xiaoyu Zhang; Jianwen Li; Yanhong Huang; Jianqi Shi (J. Log. Comput., 2024)