Guoqiang Li

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

 

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

RESEARCH INTERESTS

formal verification, programming language theory, data analytics, machine intelligence, smart healthcare

WORK EXPERIENCE

Associate Professor
School of Software, Shanghai Jiao Tong University

2014.01 –       

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

2016.12 –       

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

A full list of my lectures is avaiable here

Lectures in this Semester

  • X037506 Design and Analysis of Algorithms for graduates

    • 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 supervison are suggested to click here.

    REPRESENTATIVE PROJECTS

  • 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 full list of publications is available here. A list sorted by categories is available here

    Journals and Transactions:

  • Ruoyu Wang, Daniel Sun*, Guoqiang Li*, Raymond Wong, Shiping Chen. Pipeline Provenance for Cloud-Based Big Data Analytics. Software: Practice and Experience, accepted

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

  • Daniel Sun, Guoqiang Li, Yuanyuan Zhang, Liming Zhu, Raj Gaire. Statistically Managing Cloud Operations for Latency-tail-tolerance in IoT-Enabled Smart Cities. Journal of Parallel and Distributed Computing, Vol. 127, 184-195, 2019

  • Chenxiao Dou, Yi Cui, Daniel Sun, Raymond Wong, Muhammad Atif, Guoqiang Li, Rajiv Ranjan. Unsupervised Blocking and Probabilistic Parallelisation for Record Matching of Distributed Big Data. Journal of Supercomputing, Vol. 75(2), 623-645, 2019

  • Daniel Sun, Alan Fekete, Vincent Gramoli, Guoqiang Li, Xiwei Xu, Liming Zhu. R2C: Robust Rolling-Upgrade in Clouds. IEEE Transactions on Dependable and Secure Computing, Vol. 15(5), 811-823, 2018

  • 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

  • Haitao Zhang, Guoqiang Li*, Daniel Sun, Yonggang Lu. Verifying Deterministic Scheduler based Cooperative Software: a SMT-based Bounded Model Checking Approach. Journal of Systems Architecture, Vol. 81, 7-16, 2017

  • 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

  • Xiuting Tao, Guoqiang Li*, Daniel Sun, Hongming Cai. A Game-Theoretic Model and Analysis of Data Exchange Protocols for Internet of Things in Clouds. Future Generation Computer Systems, Vol. 76, 582-589, 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

  • Daniel Sun, Min Fu, Liming Zhu, Guoqiang Li and Qinghua Lu. Non-Intrusive Anomaly Detection with Streaming Metrics and Logs for DevOps in Public Clouds. IEEE Transactions on Emerging Topics in Computing, Vol. 4(2), 278 - 289, 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)

    • Conferences and Workshops:

  • 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), accepted, 2019

  • Haitao Zhang, Ayang Tuo, Guoqiang Li. Model Checking is Possible to Verify Large-scale Vehicle Distributed Application Systems. In Proceedings of the 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE'19), accepted, 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

  • Yun Guo, Daniel Sun, Guoqiang Li, Shiping Chen. Examine Manipulated Datasets with Topology Data Analysis: A Case Study. In Proceedings of the 20th International Conference on Information and Communications Security (ICICS'18), LNCS 11149, 358-373, 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

  • Chenxiao Dou, Daniel Sun, Guoqiang Li, Raymond K. Wong. Active Learning with Density-Initialized Decision Tree for Record Matching. In Proceedings of the 29th International Conference on Scientific and Statistical Database Management (SSDBM'17), ACM, 14:1-14:12, 2017

  • Chenxiao Dou, Daniel Sun, Yi-Cheng Chen, Guoqiang Li, Jianquan Liu. Probabilistic Parallelisation of Blocking Non-matched Records for Big Data. In Proceedings of the 3rd International Workshop on Pattern Mining and Application of Big Data (BigPMA'16 @ BigData'16), IEEE Society, 3465-3473, 2016 (Best paper award!)

  • Ruoyu Wang, Daniel Sun, Guoqiang Li, Muhammad Atif, Surya Nepal. LogProv: Logging Events as Provenance of Big Data Analytics Pipelines with Trustworthiness Evaluation. In Proceedings of the 4th IEEE International Conference on Big Data (BigData'16), IEEE Society, 1402-1411, 2016

  • Bingbing Fang, Guoqiang Li, Daniel Sun, Hongming Cai. Schedulability Analysis of Timed Regular Tasks by an Under-Approximation on WCET. In Proceedings of the 2nd Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA'16), LNCS 9984, 147-162, 2016

  • 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, Xiaojuan Cai, Shoji Yuen. Modeling and Analysis of Real-Time Systems with Mutex Components. In Proceedings of the 24th IEEE International Parallel and Distributed Processing Symposium, Workshops and Phd Forum (APDCM'10 @ IPDPS'10) , IEEE Society, 1-8, 2010

  • 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 [Extended Version]

  • 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 [Extended Version]

    • Theses:

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

  • Formal Research of Security Protocols Based on Process Calculus. Master Thesis, March, 2005. In Chinese [PDF]

    • ACADEMIC ACTIVITIES


    PC Member

  • The 4th Chinese Conference on Formal Methods and Applications (FMAC'19)

  • The 2019 IEEE International Conference on e-Business Engineering (ICEBE'19)

  • The 2019 Annual Conference on Software Analysis, Testing and Evolution (SATE'19)

  • The 5th Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA'19)

  • The 13th International Symposium on Theoretical Aspects of Software Engineering (TASE'19)


    • Organization Chair

  • FMAC'17


    • PC Member

  • 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: Tuesday, Apr. 25, 2017.