The Validation and Verification of WSCDL. - Geguang Pu; Jianqi Shi; Zheng Wang 005; Lu Jin; Jing Liu 012; Jifeng He 001 (APSEC, 2007)

Modeling and Verifying the Code-Level OSEK/VDX Operating System with CSP. - Yanhong Huang; Yongxin Zhao; Longfei Zhu; Qin Li 002; Huibiao Zhu; Jianqi Shi (TASE, 2011)

Formalizing Application Programming Interfaces of the OSEK/VDX Operating System Specification. - Longfei Zhu; Min Zhang 002; Yanhong Huang; Jianqi Shi; Huibiao Zhu (TASE, 2011)

ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System. - Jianqi Shi; Jifeng He 001; Huibiao Zhu; Huixing Fang; Yanhong Huang; Xiaoxian Zhang (ICECCS, 2012)

xBIL - A Hardware Resource Oriented Binary Intermediate Language. - Jianqi Shi; Longfei Zhu; Huixing Fang; Jian Guo 005; Huibiao Zhu; Xin Ye (ICECCS, 2012)

ESF - An Extensive Service Foundation from Internet of Things Perspective. - Jianqi Shi; Xin Ye; Liangyu Chen 001; Pei Zhang; Ningkang Jiang (ISORC Workshops, 2012)

Investigating Time Properties of Interrupt-Driven Programs. - Yanhong Huang; Yongxin Zhao; Jianqi Shi; Huibiao Zhu; Shengchao Qin (SBMF, 2012)

Formal Verification and Simulation: Co-verification for Subway Control Systems. - Huixing Fang; Jian Guo 005; Huibiao Zhu; Jianqi Shi (TASE, 2012)

Binary Code Level Verification for Interrupt Safety Properties of Real-Time Operating System. - Jianqi Shi; Longfei Zhu; Yanhong Huang; Jian Guo 005; Huibiao Zhu; Huixing Fang; Xin Ye (TASE, 2012)

A Denotational Model for Interrupt-Driven Programs. - Yanhong Huang; Yongxin Zhao; Jianqi Shi; Huibiao Zhu (ICST Workshops, 2013)

A Timing Verification Framework for AUTOSAR OS Component Development Based on Real-Time Maude. - Longfei Zhu; Peng Liu; Jianqi Shi; Zheng Wang 005; Huibiao Zhu (TASE, 2013)

Apricot - An Object-Oriented Modeling Language for Hybrid Systems - Huixing Fang; Huibiao Zhu; Jianqi Shi (CoRR, 2013)

Modeling and Verification of CAN Bus with Application Layer using UPPAAL. - Can Pan; Jian Guo 005; Longfei Zhu; Jianqi Shi; Huibiao Zhu; Xinyun Zhou (TTSS, 2013)

pIML - An Interrupt Program Modelling Language for Real-Time and Embedded Systems. - Xin Li 010; Yanhong Huang; Jianqi Shi; Jian Guo 005; Huibiao Zhu; Yuanmin Xu (APSEC (1), 2014)

Modeling and Verifying the TTCAN Protocol Using Timed CSP. - Qinwen Ran; Xi Wu 005; Xin Li 010; Jianqi Shi; Jian Guo 005; Huibiao Zhu (TASE, 2014)

A formal framework for service mashups with dynamic service selection. - Qin Li 002; Jianqi Shi; Huibiao Zhu (Innov. Syst. Softw. Eng., 2014)

Formal verification and simulation for platform screen doors and collision avoidance in subway control systems. - Huixing Fang; Jianqi Shi; Huibiao Zhu; Jian Guo 005; Kim Guldstrand Larsen; Alexandre David (Int. J. Softw. Tools Technol. Transf., 2014)

An Object-Oriented Language for Modeling of Hybrid Systems. - Huixing Fang; Huibiao Zhu; Jianqi Shi (HASE, 2015)

GPU Accelerated On-the-Fly Reachability Checking. - Zhimin Wu; Yang Liu 003; Jun Sun 001; Jianqi Shi; Shengchao Qin (ICECCS, 2015)

Formal Analysis of MAC in IEEE 802.11p with Probabilistic Model Checking. - Conghua Zhou; Yong Wang; Meiling Cao; Jianqi Shi; Yang Liu 003 (TASE, 2015)

Semantic theories of programs with nested interrupts. - Yanhong Huang; Jifeng He 001; Huibiao Zhu; Yongxin Zhao; Jianqi Shi; Shengchao Qin (Frontiers Comput. Sci., 2015)

Formalization and Verification of the Powerlink Protocol Using CSP. - Haiping Pang; Ju Li; Yijia Ruan; Yanhong Huang; Jianqi Shi; Shengchao Qin (APSEC, 2016)

Decomposition and Collaboration of Industrial Control System with Resource Constraints. - Ju Li; Jiawen Xiong; Xia Mao; Jianqi Shi; Xin Ye; Yanhong Huang (ICECCS, 2017)

A New Parallel Approach for Reachability Analysis of Pushdown Models. - Lingjie Shu; Jianqi Shi; Xin Ye; Ningkang Jiang; Yichun Li (ICMSS, 2017)

GANFuzz: a GAN-based industrial network protocol fuzzing framework. - Zhicheng Hu; Jianqi Shi; Yanhong Huang; Jiawen Xiong; Xiangxing Bu (CF, 2018)

Efficient Parallel CTL Model-Checking for Pushdown Systems. - Xinyu Chen; Hansheng Wei; Xin Ye; Li Hao; Yanhong Huang; Jianqi Shi (ISPA/IUCC/BDCloud/SocialCom/SustainCom, 2018)

Parallel Model Checking on Pushdown Systems. - Hansheng Wei; Xinyu Chen; Xin Ye; Neng Fu; Yanhong Huang; Jianqi Shi (ISPA/IUCC/BDCloud/SocialCom/SustainCom, 2018)

ParaMoC: A Parallel Model Checker for Pushdown Systems. - Hansheng Wei; Xin Ye; Jianqi Shi; Yanhong Huang (ICA3PP (2), 2019)

SeqFuzzer: An Industrial Protocol Fuzzing Framework from a Deep Learning Perspective. - Hui Zhao; Zhihui Li 005; Hansheng Wei; Jianqi Shi; Yanhong Huang (ICST, 2019)

Automated Mining and Checking of Formal Properties in Natural Language Requirements. - Xingxing Pi; Jianqi Shi; Yanhong Huang; Hansheng Wei (KSEM (2), 2019)

Scade2Nu : A Tool for Verifying Safety Requirements of SCADE Models with Temporal Specifications. - Jian Shi; Jianqi Shi; Yanhong Huang; Jiawen Xiong; Qing She (REFSQ Workshops, 2019)

CNN-based Super-resolution Reconstruction for Traffic Sign Detection. - Fan Wang; Jianqi Shi; Xuan Tang; Jielong Guo; Peidong Liang; Yuanzhi Feng (SSCI, 2019)

Automated Test Generation for IEC 61131-3 ST Programs via Dynamic Symbolic Execution. - Li Hao; Jianqi Shi; Ting Su 001; Yanhong Huang (TASE, 2019)

KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification. - Yanhong Huang; Xiangxing Bu; Gang Zhu; Xin Ye; Xiaoran Zhu; Jianqi Shi (IEEE Access, 2019)

An Intelligent Fuzzing Data Generation Method Based on Deep Adversarial Learning. - Zhihui Li 005; Hui Zhao; Jianqi Shi; Yanhong Huang; Jiawen Xiong (IEEE Access, 2019)

A Decomposition-Based Development Method for Industrial Control Systems. - Jiawen Xiong; Ju Li; Jianqi Shi; Yanhong Huang (IEEE Access, 2019)

A Feasibility Analysis Framework of Time-Sensitive Networking Using Real-Time Calculus. - Peng Zhang 055; Yu Liu; Jianqi Shi; Yanhong Huang; Yongxin Zhao (IEEE Access, 2019)

A Novel Deep Intrusion Detection Model Based On a Convolutional Neural Network. - Neng Fu; Nuerbiye Kamili; Yanhong Huang; Jianqi Shi (Aust. J. Intell. Inf. Process. Syst., 2019)

Fault Diagnosis of Simplified Fault Trees using State Transition Diagrams. - Mingyue Jiao; Yanhong Huang; Jianqi Shi; Fangda Cai; Rongfeng Lin (APSEC, 2020)

VARF: Verifying and Analyzing Robustness of Random Forests. - Chaoqun Nie; Jianqi Shi; Yanhong Huang (ICFEM, 2020)

A Novel Self-Attention Based Automatic Code Completion Neural Network. - Bohao Wang; Wanyou Lv; Jianqi Shi; Yanhong Huang (SEKE, 2020)

Modeling and Verification of A Timing Protection Mechanism in the OSEK/VDX OS using CSP. - Yanhong Huang; Haiping Pang; Jianqi Shi (Formal Aspects Comput., 2020)

Data Flow Testing for PLC Programs via Dynamic Symbolic Execution. - Weigang He; Xia Mao; Ting Su 001; Yanhong Huang; Jianqi Shi (APSEC, 2021)

A Formal Method for Evaluating the Performance of TSN Traffic Shapers using UPPAAL. - Wang Guo; Yanhong Huang; Jianqi Shi; Zhe Hou; Yang Yang 141 (LCN, 2021)

Dynamically Detecting Invariants for Automatic Testing PLC Programs (S). - Zeyu Lu; Xia Mao; Yanhong Huang; Jianqi Shi; Yang Yang 141 (SEKE, 2021)

Tree Ensemble Property Verification from A Testing Perspective. - Bohao Wang; Zhe Hou; Gelin Zhang; Jianqi Shi; Yanhong Huang (SEKE, 2021)

A Timed Automata based Automatic Framework for Verifying STL Properties of Simulink Models. - Miao Tian; Jianqi Shi; Zhe Hou; Yanhong Huang; Shengchao Qin (TASE, 2021)

General past-time linear temporal logic specification mining. - Jianqi Shi; Jiawen Xiong; Yanhong Huang (CCF Trans. High Perform. Comput., 2021)

Extracting Optimal Explanations for Ensemble Trees via Logical Reasoning. - Gelin Zhang; Zhe Hou; Yanhong Huang; Jianqi Shi; Hadrien Bride; Jin Song Dong; Yongsheng Gao 001 (CoRR, 2021)

A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems. - Jingwen Xu; Yanhong Huang; Jianqi Shi; Shengchao Qin (J. Comput. Sci. Technol., 2021)

A deep convolution generative adversarial networks based fuzzing framework for industry control protocols. - Wanyou Lv; Jiawen Xiong; Jianqi Shi; Yanhong Huang; Shengchao Qin (J. Intell. Manuf., 2021)

Automated test generation for IEC 61131-3 ST programs via dynamic symbolic execution. - Weigang He; Jianqi Shi; Ting Su 001; Zeyu Lu; Li Hao; Yanhong Huang (Sci. Comput. Program., 2021)

Safety Verification of IEC 61131-3 Structured Text Programs. - Jiawen Xiong; Xiangxing Bu; Yanhong Huang; Jianqi Shi; Weigang He (IEEE Trans. Ind. Informatics, 2021)

A Federated Model Personalisation Method Based on Sparsity Representation and Clustering. - Hailin Yang; Yanhong Huang; Jianqi Shi; Fangda Cai (SEKE, 2022)

Parallel computational tree logic model-checking on pushdown systems. - Xin Ye; Jianqi Shi; Yanhong Huang; Qin Li; Hansheng Wei; Xinyu Chen (Concurr. Comput. Pract. Exp., 2022)

MUC-driven Feature Importance Measurement and Adversarial Analysis for Random Forest. - Shucen Ma; Jianqi Shi; Yanhong Huang; Shengchao Qin; Zhe Hou (CoRR, 2022)

Minimal-unsatisfiable-core-driven Local Explainability Analysis for Random Forest. - Shucen Ma; Jianqi Shi; Yanhong Huang; Shengchao Qin; Zhe Hou (Int. J. Softw. Informatics, 2022)

A refinement development approach for enhancing the safety of PLC programs with Event-B. - Xia Mao; Yueling Zhang; Jianqi Shi; Yanhong Huang; Qin Li 002 (Sci. Comput. Program., 2022)

Programmable Logic Controllers Past Linear Temporal Logic for Monitoring Applications in Industrial Control Systems. - Xia Mao; Xin Li 109; Yanhong Huang; Jianqi Shi; Yueling Zhang (IEEE Trans. Ind. Informatics, 2022)

Improving Single-Step Adversarial Training By Local Smoothing. - Shaopeng Wang; Yanhong Huang; Jianqi Shi; Yang Yang 141; Xin Guo (IJCNN, 2023)

A Tool for Transforming SysML State Machine into Uppaal Automatically. - Shaopeng Wang; Jianqi Shi; Yanhong Huang; Yang Yang 141 (SMC, 2023)

Extracting optimal explanations for ensemble trees via automated reasoning. - Gelin Zhang; Zhé Hóu; Yanhong Huang; Jianqi Shi; Hadrien Bride; Jin Song Dong; Yongsheng Gao 001 (Appl. Intell., 2023)

A Federated Framework for Edge Computing Devices with Collaborative Fairness and Adversarial Robustness. - Hailin Yang; Yanhong Huang; Jianqi Shi; Yang Yang 141 (J. Grid Comput., 2023)

Graph Convolutional Network Robustness Verification Algorithm Based on Dual Approximation. - Dongdong An; Hao Zhang; Qin Zhao; Jing Liu; Jianqi Shi; Yanhong Huang; Yang Yang 141; Xu Liu; Shengchao Qin (ICFEM, 2024)

NL2CTL: Automatic Generation of Formal Requirements Specifications via Large Language Models. - Mengyan Zhao; Ran Tao; Yanhong Huang; Jianqi Shi; Shengchao Qin; Yang Yang 141 (ICFEM, 2024)

SELus: Towards Spatio-Temporal Modeling and Quantitative Evaluation for Cyber-Physical Systems. - Quanguo Zhang; Jing Liu; Mingxing Liu; Yanhong Huang; Rongbin Hou; Jianqi Shi (SMC, 2024)

Static Code Analysis of IEC 61131-3 ST Programs via Symbolic Execution. - Mengyan Zhao; Yanhong Huang; Jianqi Shi; Yinghao Chen; Yang Yang 141 (SMC, 2024)

OpenECAD: An efficient visual language model for editable 3D-CAD design. - Zhe Yuan; Jianqi Shi; Yanhong Huang (Comput. Graph., 2024)

OpenECAD: An Efficient Visual Language Model for Computer-Aided Design. - Zhe Yuan; Jianqi Shi; Yanhong Huang (CoRR, 2024)

Computing minimal unsatisfiable core for LTL over finite traces. - Tong Niu; Shengping Xiao; Xiaoyu Zhang; Jianwen Li; Yanhong Huang; Jianqi Shi (J. Log. Comput., 2024)

Automated Test Cases Generator for IEC 61131-3 Structured Text Based Dynamic Symbolic Execution. - Jianqi Shi; Yinghao Chen; Qin Li 002; Yanhong Huang; Yang Yang 141; Mengyan Zhao (IEEE Trans. Computers, 2024)

SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation. - Junjie Sheng; Yanqiu Lin; Jiehao Wu; Yanhong Huang; Jianqi Shi; Min Zhang; Xiangfeng Wang (NIER@ICSE, 2025)