● 2005.4-2008.3，日本北陆先端科学技术大学院大学信息科学学院，工学博士

● 2002.9-2005.3，kaiyun官网入口计算机科学与工程系，工学硕士

● 1997.9-2001.7，太原理工大学计算机科学与工程系，工学学士

● 2025.1- 至今，kaiyun官网入口，副教授，博士生导师

● 2013.12- 2024.12，kaiyun官网入口软件学院，副教授，博士生导师

● 2016.12-2020.3，日本九州大学智慧移动研究与开发中心，客座副教授

● 2015.7-2016.7，英国牛津大学计算机科学系，访问学者

● 2009.4- 2013.12，kaiyun官网入口软件学院，讲师

● 2009.12-2010.12，国家自然科学基金委员会国际合作局西欧处，兼聘 

● 2008.4-2009.3，名古屋大学信息科学研究科，博士后研究员

● SE3308，算法设计，本科生专业基础课

● EI6303，算法设计与分析，研究生专业基础课程

已结束课程

● AI1401，算法设计与分析，数学学院本科生课程，2025

● SE2324，计算机科学的数学基础，本科生课程， 2021-2023

● SE3352，算法设计（2学分），本科生课程， 2021-2023

● SE121，算法设计与实现，本科生课程， 2020

● SE222，算法原理，本科生课程， 2016-2019

● SE226，可计算理论，本科生课程，2012-2014

● GE6001, 科学写作、规范与伦理，研究生课程，2019-2024

● X037515, 程序语言理论，研究生课程，2017

Conferences and Workshops:

● Shuyang Tang, Sherman S. M. Chow, Hongfei Fu, Zihan Guo, Guoqiang Li. Staged Multi-Step UTXO Workflows via Recursive Invariants. OOPSLA'26

● Jingyang Li, Xin Chen, Hongfei Fu, Guoqiang Li . Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation. UAI'26 

● Ling-I Wu, Jian Tong, Yu Sun, Xuan Gao, Xu Guo, Qipeng Guo, Kai Chen, Guoqiang Li . Reasoning Compartmentalization: Bridging the Concretization Gap via Abstraction-based Routing . ICML'26 

● Ling-I Wu, Minyu Chen, Jingyang Li, Xi Chang, Guoqiang Li  . Think Earlier, Not Longer: Prompt Optimization via Reducing Unhealthy Exploration. ACL'26 findings

● Ling-I Wu, Weijie Wu, Minyu Chen, Jianxin Xue, Guoqiang Li . Co-Eval: Augmenting LLM-based Evaluation with Machine Metrics. EMNLP'25

● Haoyu Wei, Jingyu Ke, Ruibang Liu, and Guoqiang Li . ZK-ProVer: Proving Programming Verification in Non-Interactive  Zero-Knowledge Proofs. ICFEM'25 

● Minyu Chen, Guoqiang Li , Ling-I Wu, Ruibang Liu. DCE-LLM: Dead Code Elimination with Large Language Models. NAACL'25

● Jingyu Ke, Hongfei Fu, Hongming Liu, Zhouyue Sun, Liqian Chen and Guoqiang Li. Affine Disjunctive Invariant Generation with Farkas' Lemma.  VMCAI'25

● Jingyang Li, Guoqiang Li . HOBAT: Batch Verification for Homogeneous Structural Neural Networks. ASE'23

● Minyu Chen, Guoqiang Li , Chen Ma, Jingyang Li, Hongfei Fu. Repo4QA: Answering Coding Questions via Dense Retrieval on GitHub Repositories. COLING'22

● Hongming Liu, Hongfei Fu, Zhiyong Yu, Jiaxin Song, Guoqiang Li. Scalable Linear Invariant Generation with Farkas Lemma. OOPSLA'22

● Jieshan Chen, Mulong Xie, Zhenchang Xing, Chunyang Chen, Xiwei Xu, Liming Zhu, Guoqiang Li. Object Detection for Graphical User Interface: Old Fashioned or Deep Learning or a Combination?. FSE'20

● Jieshan Chen, Chunyang Chen, Zhenchang Xing, Xiwei Xu, Liming Zhu, Guoqiang Li , Jinshui Wang. Unblind Your Apps: Predicting Natural-Language Labels for Mobile GUI Components by Deep Learning. ICSE'20 (Distinguished paper award!)

● Dehai Zhao, Zhenchang Xing, Chunyang Chen, Xiwei Xu, Liming Zhu, Guoqiang Li , Jinshui Wang. Seenomaly: Vision-Based Linting of GUI Animation Effects Against Design-Don't Guidelines.ICSE'20

● Xiaoxue Ren, Zhenchang Xing, Xin Xia, Guoqiang Li, Jianling Sun. Discovering, Explaining and Summarizing Controversial Discussions in Community Q&A Sites. ASE'19

● Dehai Zhao, Zhenchang Xing, Chunyang Chen*, Xin Xia*, Guoqiang Li . ActionNet: Vision-based Workflow Action Recognition From Programming Screencasts. ICSE'19

● Haitao Zhang, Ayang Tuo, Guoqiang Li. Model Checking is Possible to Verify Large-scale Vehicle Distributed Application Systems. DATE'19

● Chunyang Chen, Xi Chen, Jiamou Sun, Zhenchang Xing, Guoqiang Li . Data-Driven Proactive Policy Assurance of Post Quality in Community Q&A Sites. CSCW'18

Journals and Transactions:

● Jingyang Li, Guoqiang Li . MUC-G4: Accelerating Incremental Verification of Compressed Neural Networks via Minimal UNSAT Core Reuse. ACM Transactions on Embedded Computing Systems. accepted

● Zhouyue Sun, Yuchen Li, Hongfei Fu, Guoqiang Li. Modular Invariant Generation via Constraint Solving. Journal of Systems Architecture, Vol. 178, 103884, 2026

● Minyu Chen, Ling-I Wu, Ruibang Liu, Xi Chang, Jianxin Xue, Guoqiang Li . DCoL-A: Agentic Dual Chain of Thinking Helps LLMs Pretend Logic Solvers. Journal of Systems Architecture, Vol. 175, 103780, 2026

● Qizhe Yang, Boxuan Liang, Hao Chen, Guoqiang Li . AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs. Formal Aspects of Computing, Vol. 38(1), Article 11, 2026

● Ruibang Liu, Minyu Chen, Ling-I Wu, Jingyu Ke, Guoqiang Li . Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models. Science of Computer Programming, 103387, Vol. 248, 2026

● Ruibang Liu, Hongming Liu, Guoqiang Li . Optimization of Farka's Lemma-Based Linear Invariant Generation Using Divide-and-Conquer with Pruning. Science of Computer Programming, 103361, Vol. 247, 2026

● Guoqiang Li , Qizhe Yang, Jinhao Tan, Ying Zhao. BPPChecker: An SMT-based Model Checker on Basic Parallel Processes. Formal Aspects of Computing, Vol. 37(3), Article 21, 2025

● Jingyang Li, Guoqiang Li . The Triangular Trade-off between Robustness, Accuracy and Fairness in Deep Neural Networks: A Survey. ACM Computing Surveys, Vol. 57(6),  2025

● Sinka Gao, Guoqiang Li , Hongfei Fu. ZKWASM: A ZKSNARK WASM Emulator. IEEE Transactions on Services Computing, Vol. 17(6), 4508-4521, 2024

● Chenhao Shi, Ruibang Liu, Hao Chen, Guoqiang Li , Sinka Gao. RNA: R1CS Normalization Algorithm Based on Data Flow Graphs for Zero-Knowledge Proofs. Formal Aspects of Computing, Vol. 36(4), 2024

● Suyu Ma, Zhenchang Xing, Chunyang Chen*, Cheng Chen, Lizhen Qu, Guoqiang Li . Easy-to-Deploy API Extraction by Multi-Level Feature Embedding and Transfer Learning. IEEE Transactions on Software Engineering, Vol. 47(10), 2021

中文期刊:

● 王麒扬，李璟旸，李国强. 面向领域自适应扰动的神经网络鲁棒性形式验证. 软件学报，已接收

● 吴志文，李国强. 基于非交互式Petri网的异步程序验证模型和方法. 软件学报， 34(8)：3674-3685，2023

● 赵樱，谭锦豪，李国强. 基于基本并行进程的异步通信程序的验证方法. 软件学报，33(8)：2782-2796，2022

● 谭锦豪，李国强. 基本并行进程活性的限界模型检测. 软件学报，31(8)：2388-2403，2020,

● 丁如江, 李国强. 非交互式Petri网可覆盖性验证的高效实现. 软件学报，30(7)：1939-1952，2019

● 李春淼, 蔡小娟, 李国强. 良结构下推系统的可覆盖性问题的下界. 软件学报，29(10)：3009-3020，2018

● 傅育熙, 李国强, 田聪. 形式化方法的理论基础专题前言. 软件学报，29(6)：1515-1516，2018

● 叶聪聪, 李国强, 蔡鸿明, 顾永跟. 区块链的安全检测模型. 软件学报，29(5)：1348-1359，2018

● 杨启哲, 李国强. 基于通信Petri网的异步通信程序验证模型. 软件学报，28(4)：804-818，2017

● 刘立, 李国强. 异步多进程时间自动机的可覆盖性问题. 软件学报，28(5)：1080-1090，2017

● 2026.01-2029.12 零知识证明电路程序的形式验证方法与实现，国家自然科学基金面上项目，62572294，主持

● 2026.01-2030.12 SAT算法理论与新型求解器，国家自然科学基金重点项目，62532014，主要参与

● 2024.10-2025.10 通用零知识虚拟机与高效区块链累加器研究，上海市“科技创新行动计划”区块链关键技术攻关专项项目，24BC3200200，主要参与

● 2021.10-2024.09 深度学习系统的高效可认证的形式化验证技术，国家自然科学基金国际合作中以项目，62161146001，主要参与

● 2019.01-2022.12 基于基本并发进程的异步通讯程序的验证模型与高效算法，国家自然科学基金面上项目，61872232，主持

● 2018.01-2022.12 安全攸关软件系统的可靠性保障研究，国家自然科学基金重点项目，61732013，子课题负责

● 2017.01-2017.12 异步通讯程序的程序分析理论与方法，国家自然科学基金面上项目，61672340，主持

● 2015.01-2018.12 时间敏感下推系统可达性的验证问题，国家自然科学基金面上项目，61472240，主持

● 2012.01-2014.12 基于具有时间性质的自动机模型检测的程序分析方法，国家自然科学基金青年基金，61100052，主持

● 软件工程国际会议 ICSE 2020（CCF A） 获 杰出论文奖（Distinguished Paper Award）

● 2025年 HCI高被引论文

● 中国计算机学会形式化方法专委会常务委员 （2024-2027）

● 中国人工智能学会人工智能逻辑专委会学术委员

● 中国中文信息学会语言与知识计算专委会学术委员

● 中国图像图形学会智能边缘计算专委会学术委员

● 上海计算机学会理论计算机科学专委会副主任 （2024-2028）