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 and intelligence, smart healthcare
WORK EXPERIENCE
TEACHING
A full list of my lectures is avaiable here
Lectures in this Semester
EDUCATIONAL BACKGROUND
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
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:
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, accepted
Haitao Zhang, Guoqiang Li*, Zhuo Cheng, Jinyun Xue. Verifying OSEK/VDX Automotive Applications: A Spin-Based Model Checking Approach. Software: Testing, Verification and Reliability, accepted
Congcong Ye, Guoqiang Li*, Hongming Cai, Yonggen Gu. Evaluating the Safety of Blockchain. Journal of Software (软件学报), accepted
Guoqiang Li*, Li Liu, Akira Fukuda. Asynchronous Multi-Process Timed Automata. Software Quality Journal, accepted
Chunmiao Li, Xiaojuan Cai, Guoqiang Li*. Lower Bound for Coverability Problem of Well-Structured Pushdown Systems. Journal of Software (软件学报), accepted
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, accepted
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, accepted
Ling Fang, Chunyan Mu, Zhuo Cheng, Guoqiang Li*. Evaluation of Redundancy Based System: A Model Checking Approach. SCIENCE CHINA Information Sciences, 61(6), 069101, 2018
Ruoyu Wang, Guoqiang Li*, Jianwen Xiang, Hongming Cai. A Customized Automata Algorithm and Toolkit for Language Learning and Application. International Journal of Big Data Intelligence, Vol. 5 (1&2), 114-123, 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
Yanlong Li, Guoqiang Li, Xiaoju Dong. A Survey on Visualization of Tree Comparison. Journal of Software (软件学报), in Chinese, Vol. 27 (5), 1074-1090, 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
Xiuting Tao, Yonggen Gu and Guoqiang Li. A Formal Game-Theoretic Model for Rational Exchange Protocol. Advanced Materials Research, Vol. 204-210, 2033-2040, 2011
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:
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), accepted
Xiuting Tao, Guoqiang Li. The Complexity of Linear-time Temporal Logic Model Repair. In Proceedings of the 7th International Workshop on SOFL + MSVL (SOFL+MSVL'17), accepted
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
Junli Yang, Bo Song, Bing Yan, Guoqiang Li. A Novel Hidden Markov Model for Genome-Wide Association Studies. In Proceedings of the 3rd IEEE International Workshop on Software Engineering and Knowledge Management (SEKM'17 @ QRS'17), IEEE Society, 500-506, 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
Yuwei Wang, Xiuting Tao, Guoqiang Li. On Termination and Boundedness of Nested Updatable Timed Automata with One Updatable Clock. In Proceedings of the 6th International Workshop on SOFL + MSVL (SOFL+MSVL'16), LNCS 10189, 15-31, 2016
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
Ruoyu Wang, Guoqiang Li, Daniel Sun, Jianwen Xiang, Hongming Cai. CAT: A Customized Automata Toolkit. In Proceedings of the 2nd IEEE International Workshop on Software Engineering and Knowledge Management (SEKM'16 @ QRS'16), IEEE Society, 171-177, 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
Yunqing Wen, Guoqiang Li, Shoji Yuen. On Reachability Analysis of Updatable Timed Automata with One Updatable Clock. In Proceedings of the 5th International Workshop on SOFL + MSVL (SOFL+MSVL'15), LNCS 9559, 147-161, 2015
Bingbing Fang, Guoqiang Li, Ling Fang, Jianwen Xiang. A Refined Algorithm for Reachability Analysis of Updatable Timed Automata. In Proceedings of the 1st IEEE International Workshop on Software Engineering and Knowledge Management (SEKM'15 @ QRS'15), IEEE Society, 230-236, 2015
Yunqing Wen, Guoqiang Li, Shoji Yuen. An Over-Approximation Forward Analysis for Nested Timed Automata. In Proceedings of the 4th International
Workshop on SOFL + MSVL (SOFL+MSVL'14), LNCS 8979, 62-80, 2014
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
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.