Guoqiang Li

Associate Professor, Ph.D.(JAIST,2008)
School of Computer Science,
Shanghai Jiao Tong University,
800 Dongchuan Rd., Minhang Dist., Shanghai, 200240 China

 

[Research Interests] [Experience] [Teaching] [Education] [Students] [Projects] [Publications] [Activities] [DBLP] [Contact Me]

RESEARCH INTERESTS

formal verification
programming language theory
zero-knowledge proofs and their applications
knowledge reasoning and verification
intelligent system verification and security

A detailed list of current running projects is available at here.

WORK EXPERIENCE

Associate Professor
School of Computer Science, Shanghai Jiao Tong University

2025.01 -       

Associate Professor
School of Software, Shanghai Jiao Tong University

2014.01 - 2024.12

Guest Associate Professor
Research and Development Center for Smart Mobility, Kyushu University

2016.12-2020.03

Academic Visitor
Department of Computer Science, University of Oxford

2015.07-2016.07

Lecturer
School of Software, Shanghai Jiao Tong University

2009.04-2013.12

Liaison Staff
Bureau of International Cooperation, NSFC

2009.12-2010.12

Posdoc. Researcher
NCES, Graduate School of Information Science, Nagoya University

2008.04-2009.03

TEACHING

Present Lectures [Lecture calendar this semester]

  • SE3308, Algorithm Design, for undergraduates, autumn semester

  • AI1401, Algorithm Design and Analysis, for undergraduates from School of Mathematics, autumn semester

  • EI6303, Algorithm Design and Analysis, for graduates, spring semester

    • Past Lectures

  • SE2324, Mathematical Foundation for Computer Sciences, for undergraduates, 2021-2023

  • SE3352, Algorithm Design (2 credits), for undergraduates, 2021-2023

  • SE121, Design and Implementation of Algorithms, for undergraduates, 2020

  • SE222, Principle of Algorithms, for undergraduates, 2016-2019

  • SE226, Computability Theory, for undergraduates, 2012-2014


  • GE6001, Scientific Writing, Integrity and Ethics, for graduates, 2019-2024

  • X037515, Fundamentals of Programming Languages, for graduates, 2017

    • EDUCATIONAL BACKGROUND

    PhD., Formal Verification
    Ogawa Lab, Japan Advanced Institute of Science and Technology

    		 2005.4-2008.3

    MSc., Computer Software and Theory
    BASICS, Department of CST, Shanghai Jiao Tong University

    		 2002.9-2005.3

    BSc., Computer Software
    Department of CST, Taiyuan University of Technology

    		 1997.9-2001.7

    STUDENTS

  • A list of my students is available here

  • Those who are looking for doctorial or master supervision are suggested to click here.

    • REPRESENTATIVE PROJECTS

  • Research on Universal Zero-Knowledge Virtual Machines and Efficient Blockchain Accumulators, main contributor, Special Project on Key Technologies in Blockchain, Shanghai Science and Technology Innovation Action Plan, 2024-2025

  • Scalable and Certifiable Verification of Deep-Learning Enabled Systems, main contributor, NSFC-ISF Joint Program, 2021-2024

  • Verification Models and Efficient Algorithms of Asynchronously Communicating Programs Based on Basic Parallel Processes, PI, NSFC General Program, 2019-2022

  • Reliability of Safety Critical Software Systems, Sub-project PI, NSFC Key Program, 2018-2022

  • Theory and Methodology of Asynchronously Communicating Program Analysis, PI, NSFC General Program, 2017

  • Verification on Reachability Problem of Time-Sensitive Pushdown Systems, PI, NSFC General Program, 2015-2018

  • Methodology of Program Analysis Based on Automata Model Checking with Time Issues, PI, NSFC Youth, 2012-2014

    • SELECTED PUBLICATIONS

    A list sorted by categories is available here

    Conferences and Workshops:

  • Minyu Chen, Guoqiang Li*, Ling-I Wu, Ruibang Liu. DCE-LLM: Dead Code Elimination with Large Language Models. In Proceedings of the 2025 Annual Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics (NAACL'25), Association for Computational Linguistics, 9942-9955, 2025

  • Jingyu Ke, Hongfei Fu, Hongming Liu, Zhouyue Sun, Liqian Chen and Guoqiang Li. Affine Disjunctive Invariant Generation with Farkas' Lemma. In Proceedings of the 26th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'25), LNCS 15529, 187-213, 2025

  • Minyu Chen, Guoqiang Li*, Ling-I Wu, Ruibang Liu, Yuxin Su, Xi Chang, Jianxin Xue. Can Language Models Pretend Solvers? Logic Code Simulation with LLMs. In Proceedings of the 10th International Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA'24), LNCS 15469, 102-121, 2024

  • Yuchen Li, Hongfei Fu, Haowen Long, Guoqiang Li. Constraint Based Invariant Generation with Modular Operations. In Proceedings of the 10th International Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA'24), LNCS 15469, 64-84, 2024

  • Hongming Liu, Guoqiang Li*. Empirically Scalable Invariant Generation Leveraging Divide-and-Conquer with Pruning. In Proceedings of the 18th International Symposium on Theoretical Aspects of Software Engineering (TASE'24), LNCS 14777, 324-342, 2024

  • Jingyang Li, Guoqiang Li*. HOBAT: Batch Verification for Homogeneous Structural Neural Networks. In Proceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering (ASE'23), 1276-1287, 2023

  • Chenhao Shi, Hao Chen, Ruibang Liu, Guoqiang Li*. Data-Flow-Based Normalization Generation Algorithm of R1CS for Zero-Knowledge Proof. In Proceedings of the 28th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC'23), IEEE Society, 191-197, 2023

  • Minyu Chen, Guoqiang Li*, Chen Ma, Jingyang Li, Hongfei Fu. Repo4QA: Answering Coding Questions via Dense Retrieval on GitHub Repositories. In Proceedings of the 29th International Conference on Computational Linguistics, (COLING'22), International Committee on Computational Linguistics, 1580-1592, 2022

  • Hongming Liu, Hongfei Fu, Zhiyong Yu, Jiaxin Song, Guoqiang Li. Scalable Linear Invariant Generation with Farkas Lemma. In Proceedings of the 37th ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'22), Proceedings of the ACM on Programming Languages Vol.6 (OOPSLA2): 204-232, 2022

  • Qunhao Sha, Qizhe Yang, Guoqiang Li*. A Parallel Implementation of Liveness on Knowledge Graphs under Label Constraints. In Proceedings of the 15th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'21), IEEE Society, 103-110, 2021

  • 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?. In Proceedings of the ACM Joint Meeting on the 18th European Software Engineering Conference and the 28 Symposium on the Foundations of Software Engineering (ESEC/FSE'20), 1202-1214, 2020

  • 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. In Proceedings of the 42nd International Conference on Software Engineering (ICSE'20), 322-334, 2020 (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. In Proceedings of the 42nd International Conference on Software Engineering (ICSE'20), 1286-1297, 2020

  • Xiaoxue Ren, Zhenchang Xing, Xin Xia, Guoqiang Li, Jianling Sun. Discovering, Explaining and Summarizing Controversial Discussions in Community Q&A Sites. In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE'19), 151-162, 2019

  • Dehai Zhao, Zhenchang Xing, Chunyang Chen*, Xin Xia*, Guoqiang Li*. ActionNet: Vision-based Workflow Action Recognition From Programming Screencasts. In Proceedings of the 41st ACM/IEEE International Conference on Software Engineering (ICSE'19), 350-361, 2019

  • Haitao Zhang, Ayang Tuo, Guoqiang Li. Model Checking is Possible to Verify Large-scale Vehicle Distributed Application Systems. In Proceedings of the 26th Design, Automation & Test in Europe Conference & Exhibition (DATE'19), 594-597, 2019

  • Muhammad Jahanzeb Khan, Adeel Zafar, Valeriia Tumanian, Yue Ding, Guoqiang Li*. Object Detection Boosting using Object Attributes in Detect and Describe Framework. In Proceedings of the 31st International Conference on Tools with Artificial Intelligence (ICTAI'19), 886-893, 2019

  • Chunyang Chen, Xi Chen, Jiamou Sun, Zhenchang Xing, Guoqiang Li*. Data-Driven Proactive Policy Assurance of Post Quality in Community Q&A Sites. In Proceedings of the 21st ACM Conference on Computer-Supported Cooperative Work and Social Computing (CSCW'18), ACM, Vol. 2, 33, 2018

  • Haitao Zhang, Guoqiang Li, Xiaohong Li, Zhuo Cheng, Jinyun Xue, Shaoying Liu. An Efficient Approach for Verifying Automobile Distributed Application Systems on Timing Property. In Proceedings of the 40th International Conference on Software Engineering (ICSE'18), IEEE/ACM Society, 230-231, 2018

  • Yuwei Wang, Guoqiang Li, Shoji Yuen. Nested Timed Automata with Invariants. In Proceedings of the 3rd Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA'17), LNCS 10606, 77-93, 2017

  • Yuwei Wang, Yunqing Wen, Guoqiang Li, Shoji Yuen. Nested Timed Automata with Diagonal Constraints. In Proceedings of the 19th International Conference on Formal Engineering Methods (ICFEM'17), LNCS 10610, 396-412, 2017

  • Haitao Zhang, Zhuo Cheng, Cong Tian, Yonggang Lu, Guoqiang Li. Verifying OSEK/VDX Applications: An Optimized SMT-based Bounded Model Checking Approach. In Proceedings of the 15th IEEE/ACIS International Conference on Computer and Information Science (ACIS-ICIS'16), IEEE Society, 1-6, 2016

  • Guoqiang Li, Mizuhito Ogawa, Shoji Yuen. Nested Timed Automata with Frozen Clocks. In Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'15), LNCS 9268, 189-205, 2015

  • Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen. Nested Timed Automata . In Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'13), LNCS 8053, 168-182, 2013

  • Yizhou Zhang, Hao Lin, Guoqiang Li. Emerald: An Automated Modeling and Verification Tool for Component-Based Real-Time Systems. In Proceedings of the 12th International Conference on Quality Software (QISC'12), IEEE Society, 120-123, 2012

  • Guoqiang Li. Measuring Time Lag with Nested Preemptions and Resumptions. In Proceedings of the 1st International Workshop on Formal methOds for Real-time Distributed Systems (FORDS'12 @ ISORC'12), IEEE Society, 19-24, 2012

  • Guoqiang Li, Shoji Yuen, Masakazu Adachi.Environmental Simulation of Real-Time Systems with Nested Interrupts. In Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'09), IEEE Society, 21-28, 2009

  • Guoqiang Li, Mizuhito Ogawa. Authentication Revisited: Flaw or Not, the Recursive Authentication Protocol. In Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08), LNCS 5311, 374-385, 2008

  • Guoqiang Li, Mizuhito Ogawa. On-the-fly Model Checking of Fair Non-repudiation Protocols. In Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07), LNCS 4762, 511-522, 2007

    • Journals and Transactions:

  • 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

  • Ling-I Wu, Yuxin Su, Guoqiang Li*. Zero-Shot Construction of Chinese Medical Knowledge Graph with GPT-3.5-turbo and GPT-4. ACM Transactions on Management Information Systems, Vol. 16(2), Article 14, 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), Article 140, 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), Article 20, 2024

  • Zhiwen Wu, Guoqiang Li*. A Formal Model and Method for Verifying Asynchronous Program Based on Communication-Free Petri Net. Journal of Software (in Chinese), Vol. 34(8), 3674-3685, 2023

  • Ying Zhao, Jinhao Tan, Guoqiang Li*. Verification Method and Implementation of Asynchronously Communicating Programs Based on Basic Parallel Processes. Journal of Software (in Chinese), Vol. 33(8), 2782-2796, 2022

  • 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), 2296 - 2311, 2021

  • Jinhao Tan, Guoqiang Li*. Bounded Model Checking Liveness on Basic Parallel Processes. Journal of Software (in Chinese), Vol. 31(8), 2388-2403, 2020

  • Rujiang Ding, Guoqiang Li*. An Efficient Implementation of Coverability Verification on Communication-free Petri Net. Journal of Software (in Chinese), Vol. 30(7), 1939-1952, 2019

  • Chunmiao Li, Xiaojuan Cai, Guoqiang Li*. Lower Bound for Coverability Problem of Well-Structured Pushdown Systems. Journal of Software (in Chinese), Vol. 29(10), 3009-3020, 2018

  • Guoqiang Li*, Li Liu, Akira Fukuda. Asynchronous Multi-Process Timed Automata. Software Quality Journal, Vol. 26(3): 961-989, 2018

  • Yuxi Fu, Guoqiang Li, Cong Tian. Preface on Theoretical Foundation of Formal Methods. Journal of Software (in Chinese), Vol. 29(6), 1515-1516, 2018

  • Haitao Zhang, Guoqiang Li*, Zhuo Cheng, Jinyun Xue. Verifying OSEK/VDX Automotive Applications: A Spin-Based Model Checking Approach. Software: Testing, Verification and Reliability, Vol. 28(3), 2018

  • Congcong Ye, Guoqiang Li*, Hongming Cai, Yonggen Gu. Evaluating the Safety of Blockchain. Journal of Software (in Chinese), Vol. 29(5), 1348-1359, 2018

  • Ling Fang, Chunyan Mu, Zhuo Cheng, Guoqiang Li*. Evaluation of Redundancy Based System: A Model Checking Approach. SCIENCE CHINA Information Sciences, Vol. 61(6), 069101, 2018

  • Haitao Zhang, Zhuo Cheng, Guoqiang Li, Shaoying Liu. autoC: an Efficient Translator for Model Checking Deterministic Scheduler based OSEK/VDX Applications. SCIENCE CHINA Information Sciences, Vol. 61(5), 052102, 2018

  • Guoqiang Li*, Yunqing Wen, Shoji Yuen. Updatable Timed Automata with One Updatable Clock. SCIENCE CHINA Information Sciences, Vol. 61(1), 012102, 2018

  • Qizhe Yang, Guoqiang Li*. Model on Asynchronously Communicating Program Verification Based on Communicating Petri Nets. Journal of Software (in Chinese), Vol. 28(4), 804-818, 2017

  • Li Liu, Guoqiang Li*. The Coverability Problem of Asynchronous Multi-Process Timed Automata. Journal of Software (in Chinese), Vol. 28(5), 1080-1090, 2017

  • Yuwei Wang, Guoqiang Li* and Shoji Yuen. Nested Timed Automata with Various Clocks. Science Foundation in China, Vol. 24(2), 51-68, 2016

  • Lichao Wang, Guoqiang Li*, Zhenjiang Hu. Constructing Format-Preserving Printing from Syntax-Directed Definition. SCIENCE CHINA Information Sciences, Vol. 58 (11), 112106:1-112106:14, 2015

  • Guoqiang Li*, Xiaojuan Cai, Shoji Yuen. Modeling and Analysis of Real-Time Systems with Mutex Components. International Journal of Foundations of Computer Science (IJFCS) , Vol. 23(4), 831-851, 2012

  • Guoqiang Li*, Mizuhito Ogawa. On-the-fly model checking of security protocols and its implementation by Maude. IPSJ Transactions on Programming, Vol.48, No. SIG 10(PRO 33), 50-75, June 2007 (also appear in IPSJ Digital Courier, Vol.3, 343-368, 2007)

    • Manuscripts:

  • Haoyu Wei, Jingyu Ke, Ruibang Liu, and Guoqiang Li. ZK-ProVer: Proving Programming Verification in Non-Interactive Zero-Knowledge Proofs . Cryptology ePrint Archive, 2025/1152

  • Jingyang Li, Guoqiang Li. MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression. CoRR abs/2506.04268

  • Junyong Chen, Ling-I Wu, Minyu Chen, Xiaoying Qian, Haoze Zhu, Qiongfang Zhang, Guoqiang Li. ARCEAK: An Automated Rule Checking Framework Enhanced with Architectural Knowledge. CoRR abs/2501.14735

  • Ruibang Liu, Guoqiang Li, Minyu Chen, Ling-I Wu, Jingyu Ke. Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models. CoRR abs/2412.10483

  • Hao Chen, Minyu Chen, Ruibang Liu, Guoqiang Li, Sinka Gao. AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs. CoRR abs/2403.15676

    • Theses:

  • On-the-fly Model Checking of Security Protocols. Doctoral Thesis, March, 2008

  • Formal Research of Security Protocols Based on Process Calculus. Master Thesis, March, 2005.

    • ACADEMIC ACTIVITIES


    Senior member of China Computer Federation (CCF)

    Deputy Director of Theoretical Computer Science, Shanghai Computer Society

    Committee member

  • Standing Committee of Formal Methods, China Computer Federation

  • Technical Committee of Logics in Artificial Intelligence, Chinese Association for Artificial Intelligence

  • Technical Committee of Language and Knowledge Computing, Chinese Information Processing Society of China

  • Technical Committee of Image Intelligence and Edge Computing, China Society of Image and Graphics

  • Technical Committee of Theoretical Computer Science, Shanghai Computer Society

  • Technical Committee of Construction Internet and BIM, Chinese Society for Urban Studies


    • Organization Chair

  • SEKM'22 | SEKM'21 | SEKM'20 | FMAC'17


    • Publicity Chair

  • TASE'23 | TASE'22 | TASE'21


    • PC Member

  • CCF ChinaSoft 2025

  • The 19th China Conference on Knowledge Graph and Semantic Computing (CCKS'25)

  • the 22nd Pacific Rim International Conference on Artificial Intelligence (PRICAI'25)

  • The 14th International Joint Conference on Knowledge Graphs (IJCKG'25)

  • The 5th International Conference on Artificial Intelligence, Logic and Application (AILA'25)

  • Chinasoft'24 | PRICAI'24 | CCKS-IJCKG'24 | TASE'24 | IEEE MedAI'24 | AILA'24 | GPC'24 | CSCWD'24

  • Chinasoft'23 | SETTA'23 | CCKS'23 | TASE'23 | PRICAI'23 | IEEE MedAI'23

  • Chinasoft'22 | CCKS'22 | SETTA'22 | TASE'22 | ICTAC'22

  • Chinasoft'21 | CCKS'21 | SETTA'21 | TASE'21 | SEKM'21

  • SEKM'20 | TASE'20

  • SEKM'19 | FMAC'19 | ICEBE'19 | SATE'19 | SETTA'19 | TASE'19

  • DSA'18 | YR-FMAC'18 | ICEBE'18 | SATE'18 | SEKM'18 | ISSSR'18 | FMAC'18 | SETTA'18 | APDCM'18

  • YR-SETTA'17 | DSA'17 | ICFEM'17 | SOFL+MSVL'17 | TASE'17 | SEKM'17 | ICA3PP'17 | APDCM'17

  • FMAC'16 | YR-SETTA'16 | IS3R'16 | ICEBE'16 | SEKM'16 | SOFL+MSVL'16 | CANDAR'16 | PDAA'16 | APDCM'16 | D2D'16

  • YR-SETTA'15 | CANDAR'15 | DCIT'15 | SEKM'15 | APDCM'15 | HASE'15

  • CANDAR'14 | APDCM'14

  • PDAA'13 | CANDAR'13 | APDCM'13

  • PDAA'12 | ICNC'12 | FORDS'12 | APDCM'12

  • PDAA'11 | ICNC'11 | APDCM'11

  • PDAA'10


    • Poster Session Chair
  • APLAS'10

    • CONTACT ME

    Address: Room 1212, Software Building, 800 Dongchuan Road, Minhang District, Shanghai, 200240 China
    Phone: +86-21-3420-4167
    Email: li DOT g AT sjtu DOT edu DOT cn

    Guoqiang Li
    Last modified: Friday, Apr. 14, 2023.