Formal Approaches to Mode Conversion and Positioning for Vehicle System. - Wen Su; Fan Yang; Xiaofeng Wu; Jian Guo 005; Huibiao Zhu (COMPSAC Workshops, 2011)

Towards Denotational Semantics for Verilog in PVS. - Han Zhu; Huibiao Zhu; Si Liu 003; Jian Guo 005 (SSIRI (Companion), 2011)

xBIL - A Hardware Resource Oriented Binary Intermediate Language. - Jianqi Shi; Longfei Zhu; Huixing Fang; Jian Guo 005; Huibiao Zhu; Xin Ye (ICECCS, 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)

Modeling and Verification of AUTOSAR OS and EMS Application. - Yunhui Peng; Yanhong Huang; Ting Su 001; Jian Guo 005 (TASE, 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)

Formalization and Verification of REST on HTTP Using CSP. - Ting Yuan; Yiting Tang; Xi Wu 005; Yue Zhang; Huibiao Zhu; Jian Guo 005; Weijun Qin (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)

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)

Formalization and Verification of REST Architecture in Viewpoints. - Yiting Tang; Xi Wu 005; Huibiao Zhu; Jian Guo 005 (HASE, 2015)

Formal Verification of PKMv3 Protocol Using DT-Spin. - Xiaoran Zhu; Yuanmin Xu; Jian Guo 005; Xi Wu 005; Huibiao Zhu; Weikai Miao (TASE, 2015)

Modeling and Verifying HDFS Using CSP. - Wanling Xie; Huibiao Zhu; Xi Wu 005; Shuangqing Xiang; Jian Guo 005 (COMPSAC, 2016)

Formalization and Verification of the PKMv3 Protocol Using CSP. - Yuanmin Xu; Huibiao Zhu; Xiaoran Zhu; Xi Wu 005; Jian Guo 005; Gang Lu (COMPSAC (1), 2017)

Towards an executable semantics of automobile RTOS standard and its application to conformance verification. - Xiaoran Zhu; Min Zhang 002; Jian Guo 005 (CoRR, 2017)

Modeling and Verifying HDFS Using Process Algebra. - Wanling Xie; Huibiao Zhu; Xi Wu 005; Shuangqing Xiang; Jian Guo 005; Phan Cong Vinh (Mob. Networks Appl., 2017)

Formal Analysis of the PKMv3 Protocol. - Xiaoran Zhu; Yuanmin Xu; Xin Li 010; Jian Guo 005; Huibiao Zhu; Phan Cong Vinh (Mob. Networks Appl., 2018)

Formal Modeling and Verifying the TTCAN Protocol from a Probabilistic Perspective. - Xin Li 109; Jian Guo 005; Yongxin Zhao; Xiaoran Zhu (J. Circuits Syst. Comput., 2019)

Toward a Unified Executable Formal Automobile OS Kernel and Its Applications. - Xiaoran Zhu; Min Zhang 002; Jian Guo 005; Xin Li 010; Huibiao Zhu; Jifeng He 001 (IEEE Trans. Reliab., 2019)

SAT-Based Automata Construction for LTL over Finite Traces. - Yingying Shi; Shengping Xiao; Jianwen Li; Jian Guo 005; Geguang Pu (APSEC, 2020)

Formal Verification of a Hybrid IoT Operating System Model. - Yuqian Guan; Jian Guo 005; Qin Li 002 (IEEE Access, 2021)

Adaptive Layered Segregated Fit Scheme for Dynamic Memory Allocation. - Yuqian Guan; Jian Guo 005 (J. Circuits Syst. Comput., 2021)