Querying Process Models Based on the Temporal Relations between Tasks. - Liang Song; Jianmin Wang 001; Lijie Wen 001; Wenxing Wang; Shijie Tan; Hui Kong 004 (EDOCW, 2011)

Proving Computational Geometry Algorithms in TLA+2. - Hui Kong 004; Hehua Zhang; Xiaoyu Song; Ming Gu 001; Jiaguang Sun 001 (TASE, 2011)

Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems. - Hui Kong 004; Fei He 001; Xiaoyu Song; William N. N. Hung; Ming Gu 001 (CAV, 2013)

Efficient Semantics-Based Compliance Checking Using LTL Formulae and Unfolding. - Liang Song; Jianmin Wang 001; Lijie Wen 001; Hui Kong 004 (J. Appl. Math., 2013)

A New Barrier Certificate for Safety Verification of Hybrid Systems. - Hui Kong 004; Xiaoyu Song; Dong Han; Ming Gu 001; Jiaguang Sun 001 (Comput. J., 2014)

Abstraction-Based Parameter Synthesis for Multiaffine Systems. - Sergiy Bogomolov; Christian Schilling 001; Ezio Bartocci; Grégory Batt; Hui Kong 004; Radu Grosu (Haifa Verification Conference, 2015)

Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller. - Yu Jiang 001; Han Liu 010; Houbing Song; Hui Kong 004; Ming Gu 001; Jiaguang Sun 001; Lui Sha (FM, 2016)

Discrete Abstraction of Multiaffine Systems. - Hui Kong 004; Ezio Bartocci; Sergiy Bogomolov; Radu Grosu; Thomas A. Henzinger; Yu Jiang 001; Christian Schilling 001 (HSB, 2016)

Use runtime verification to improve the quality of medical care practice. - Yu Jiang 001; Han Liu 010; Hui Kong 004; Rui Wang 024; Mohammad Hosseini 002; Jia-Guang Sun 001; Lui Sha (ICSE (Companion Volume), 2016)

From Stateflow Simulation to Verified Implementation: A Verification Approach and A Real-Time Train Controller Design. - Yu Jiang 001; Yixiao Yang; Han Liu 010; Hui Kong 004; Ming Gu 001; Jia-Guang Sun 001; Lui Sha (RTAS, 2016)

Invariant Clusters for Hybrid Systems. - Hui Kong 004; Sergiy Bogomolov; Christian Schilling 001; Yu Jiang 001; Thomas A. Henzinger (CoRR, 2016)

Conic Abstractions for Hybrid Systems. - Sergiy Bogomolov; Mirco Giacobbe; Thomas A. Henzinger; Hui Kong 004 (FORMATS, 2017)

Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters. - Hui Kong 004; Sergiy Bogomolov; Christian Schilling 001; Yu Jiang 001; Thomas A. Henzinger (HSCC, 2017)

Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes. - Hui Kong 004; Ezio Bartocci; Thomas A. Henzinger (CAV (1), 2018)

Safety-Assured Model-Driven Design of the Multifunction Vehicle Bus Controller. - Yu Jiang 001; Han Liu 010; Houbing Song; Hui Kong 004; Rui Wang 024; Yong Guan; Lui Sha (IEEE Trans. Intell. Transp. Syst., 2018)

Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty. - Hui Kong 004; Ezio Bartocci; Yu Jiang 001; Thomas A. Henzinger (FORMATS, 2019)

Uncertainty Theory Based Reliability-Centric Cyber-Physical System Design. - Yu Jiang 001; Mingzhe Wang; Xun Jiao; Houbing Song; Hui Kong 004; Rui Wang 024; Yongxin Liu; Jian Wang 061; Jiaguang Sun 001 (iThings/GreenCom/CPSCom/SmartData, 2019)

Bounded Model Checking of Synchronous Reactive Models in Ptolemy II. - Xiaozhen Zhang; Zhaoming Yang; Hui Kong 004; Weiqiang Kong (APSEC, 2022)

Formal Verification of Hierarchical Ptolemy II Synchronous-Reactive Models with Bounded Model Checking. - Xiaozhen Zhang; Zhaoming Yang; Hui Kong 004; Weiqiang Kong (QRS, 2022)

Verification of Safety for Synchronous-Reactive System Using Bounded Model Checking. - Xiaozhen Zhang; Zhaoming Yang; Hui Kong 004; Weiqiang Kong (Int. J. Softw. Eng. Knowl. Eng., 2023)