Recent Publications

  • Avoiding the Shoals - A New Approach to Liveness Checking. Yechuan Xia, Alessandro Cimatti, Alberto Griggio, and Jianwen Li*. International Conference on Computer Aided Verification (CAV), 2024. [pdf]
  • Model-Guided Synthesis for LTL over Finite Traces. Shengping Xiao, Yongkang Li, Xinyue Huang, Yicong Xu, Jianwen Li*, Geguang Pu, Ofer Strichman and Moshe Y. Vardi. 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2024. [pdf]
  • LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems. Yibo Dong, Xiaoyu Zhang, Yicong Xu, Chang Cai, Yu Chen, Weikai Miao, Jianwen Li* and Geguang Pu*. The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023. [pdf] [Tool Demo]
  • Computing Minimal Unsatisfiable Cores for LTL over finite traces. Tong Niu, Shengping Xiao, Xiaoyu Zhang, Jianwen Li, Yanhong Huang*, and Jianqi Shi. Journal of Logic and Computation (JLC), 2023. [pdf]
  • Searching for i-Good Lemmas to Accelerate Safety Model Checking. Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li*, and Geguang Pu*. International Conference on Computer Aided Verification (CAV), 2023. [pdf]
  • FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format. Shengping Xiao, Chengyu Zhang, Jianwen Li* and Geguang Pu*. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2023. [pdf]
  • Accelerate Safety Model Checking Based on Complementary Approximate Reachability. Xiaoyu Zhang, Shengping Xiao, Yechuan Xia, Jianwen Li*, Mingsong Chen, and Geguang Pu. Transaction on Computer Aided Design (TCAD), 2022. [pdf]
  • Combining BMC and Complementary Approximate Reachability to Accelerate Bug-Finding. Xiaoyu Zhang, Shengping Xiao, Jianwen Li*, Geguang Pu, Ofer Strichman. International Conference on Computer Aided Design (ICCAD), 2022. [pdf]
  • Satisfiability checking for Mission-time LTL (MLTL). Jianwen Li, Moshe Y. Vardi and Kristin Y. Rozier. Journal of Information and Computation (INCO), 2022. [pdf]
  • On-the-fly Synthesis for LTL over Finite Traces. Shengping Xiao, Jianwen Li*, Shufang Zhu, Yingying Shi, Geguang Pu* and Moshe Vardi. AAAI Conference on Artificial Intelligence (AAAI), 2021. [pdf]

For more of my publications, please see my google scholar and DBLP.