An Assume/Guarantee Based Compositional Calculus for Hybrid CSP. - Shuling Wang 003; Naijun Zhan; Dimitar P. Guelev (TAMC, 2012)

Verifying Simulink diagrams via a Hybrid Hoare Logic Prover. - Liang Zou; Naijun Zhan; Shuling Wang 003; Martin Fränzle; Shengchao Qin (EMSOFT, 2013)

Super-Dense Computation in Verification of Hybrid CSP Processes. - Dimitar P. Guelev; Shuling Wang 003; Naijun Zhan; Chaochen Zhou (FACS, 2013)

Formal Modelling, Analysis and Verification of Hybrid Systems. - Naijun Zhan; Shuling Wang 003; Hengjun Zhao (ICTAC Training School on Software Engineering, 2013)

Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving. - Liang Zou; Jidong Lv; Shuling Wang 003; Naijun Zhan; Tao Tang 004; Lei Yuan; Yu Liu (VSTTE, 2013)

Adding Formal Meanings to AADL with Hybrid Annex. - Ehsan Ahmad; Yunwei Dong; Shuling Wang 003; Naijun Zhan; Liang Zou (FACS, 2014)

Denial-of-Service Security Attack in the Continuous-Time World. - Shuling Wang 003; Flemming Nielson; Hanne Riis Nielson (FORTE, 2014)

A Framework for Hybrid Systems with Denial-of-Service Security Attack. - Shuling Wang 003; Flemming Nielson; Hanne Riis Nielson (CoRR, 2014)

Formal Verification of Simulink/Stateflow Diagrams. - Liang Zou; Naijun Zhan; Shuling Wang 003; Martin Fränzle (ATVA, 2015)

An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems. - Shuling Wang 003; Naijun Zhan; Liang Zou (ICFEM, 2015)

Extending Hybrid CSP with Probability and Stochasticity. - Yu Peng; Shuling Wang 003; Naijun Zhan; Lijun Zhang 001 (SETTA, 2015)

Approximate Bisimulation and Discretization of Hybrid CSP. - Gaogao Yan; Li Jiao; Yangjia Li; Shuling Wang 003; Naijun Zhan (FM, 2016)

A Two-Way Path Between Formal and Informal Design of Embedded Systems. - Mingshuai Chen; Anders P. Ravn; Shuling Wang 003; Mengfei Yang; Naijun Zhan (UTP, 2016)

A Theorem Prover for Quantum Hoare Logic and Its Applications. - Tao Liu; Yangjia Li; Shuling Wang 003; Mingsheng Ying; Naijun Zhan (CoRR, 2016)

MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems. - Mingshuai Chen; Xiao Han 003; Tao Tang 004; Shuling Wang 003; Mengfei Yang; Naijun Zhan; Hengjun Zhao; Liang Zou (Provably Correct Systems, 2017)

Synthesizing SystemC Code from Delay Hybrid CSP. - Gaogao Yan; Li Jiao; Shuling Wang 003; Naijun Zhan (APLAS, 2017)

Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus. - Dimitar P. Guelev; Shuling Wang 003; Naijun Zhan (SETTA, 2017)

Modelling and Verifying Communication Failure of Hybrid Systems in HCSP. - Shuling Wang 003; Flemming Nielson; Hanne Riis Nielson; Naijun Zhan (Comput. J., 2017)

A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. - Shuling Wang 003; Naijun Zhan; Lijun Zhang 001 (Formal Aspects Comput., 2017)

ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Andrew Sogokon; Yong Kiam Tan; André Platzer; Hengjun Zhao; Xiangyu Jin; Shuling Wang 003; Naijun Zhan (ARCH@ADHS, 2018)

Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. - Junyi Liu 002; Bohua Zhan; Shuling Wang 003; Shenggang Ying; Tao Liu; Yangjia Li; Mingsheng Ying; Naijun Zhan (CAV (2), 2019)

ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Andrew Sogokon; Yong Kiam Tan; Xiangyu Jin; Bohua Zhan; Shuling Wang 003; Naijun Zhan (ARCH@CPSIoTWeek, 2019)

Unified Graphical Co-modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow. - Haolan Zhan; Qianqian Lin; Shuling Wang 003; Jean-Pierre Talpin; Xiong Xu; Naijun Zhan (UTP, 2019)

Quantum Hoare Logic. - Junyi Liu 002; Bohua Zhan; Shuling Wang 003; Shenggang Ying; Tao Liu; Yangjia Li; Mingsheng Ying; Naijun Zhan (Arch. Formal Proofs, 2019)

ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Jonathan Julián Huerta y Munive; Xiangyu Jin; Bohua Zhan; Shuling Wang 003; Naijun Zhan (ARCH, 2020)

Automatically Generating SystemC Code from HCSP Formal Models. - Gaogao Yan; Li Jiao; Shuling Wang 003; Lingtai Wang; Naijun Zhan (ACM Trans. Softw. Eng. Methodol., 2020)

ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Xiangyu Jin; Bohua Zhan; Shuling Wang 003; Naijun Zhan (ARCH@ADHS, 2021)

Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. - Bohua Zhan; Bin Gu 006; Xiong Xu; Xiangyu Jin; Shuling Wang 003; Bai Xue 001; Xiaofeng Li; Yao Chen; Mengfei Yang; Naijun Zhan (RTAS, 2021)

Formal Analysis of 5G AKMA. - Tengshun Yang; Shuling Wang 003; Bohua Zhan; Naijun Zhan; Jinghui Li; Shuangqing Xiang; Zhan Xiang; Bifei Mao (SETTA, 2021)

ARCH-COMP22 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Bohua Zhan; Huanhuan Sheng; Alexander Bentkamp; Xiangyu Jin; Shuling Wang 003; Simon Foster 001; Christian Pardillo Laursen; Jonathan Julián Huerta y Munive (ARCH@SAFECOMP, 2022)

Machine-Checked Executable Semantics of Stateflow. - Shicheng Yi; Shuling Wang 003; Bohua Zhan; Naijun Zhan (ICFEM, 2022)

Formal Analysis of 5G Authentication and Key Management for Applications (AKMA). - Tengshun Yang; Shuling Wang 003; Bohua Zhan; Naijun Zhan; Jinghui Li; Shuangqing Xiang; Zhan Xiang; Bifei Mao (J. Syst. Archit., 2022)

Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow. - Xiong Xu; Shuling Wang 003; Bohua Zhan; Xiangyu Jin; Jean-Pierre Talpin; Naijun Zhan (Theor. Comput. Sci., 2022)

ARCH-COMP23 Category Report: Hybrid Systems Theorem Proving. - Stefan Mitsch; Huanhuan Sheng; Bohua Zhan; Shuling Wang 003; Simon Foster 001; Jonathan Julián Huerta y Munive (ARCH, 2023)

A Generalized Hybrid Hoare Logic. - Naijun Zhan; Bohua Zhan; Shuling Wang 003; Dimitar P. Guelev; Xiangyu Jin (CoRR, 2023)

A denotational semantics of Simulink with higher-order UTP. - Xiong Xu; Bohua Zhan; Shuling Wang 003; Jean-Pierre Talpin; Naijun Zhan (J. Log. Algebraic Methods Program., 2023)

Semantics Foundation for Cyber-physical Systems Using Higher-order UTP. - Xiong Xu; Jean-Pierre Talpin; Shuling Wang 003; Bohua Zhan; Naijun Zhan (ACM Trans. Softw. Eng. Methodol., 2023)

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. - Shuling Wang 003; Zekun Ji; Xiong Xu; Bohua Zhan; Qiang Gao; Naijun Zhan (ICCPS, 2024)

The Design of Intelligent Temperature Control System of Smart House with MARS. - Yihao Yin; Hao Wu 085; Shuling Wang 003; Xiong Xu; Fanjiang Xu; Naijun Zhan (SETTA, 2024)

Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems. - Bohua Zhan; Xiong Xu; Qiang Gao; Zekun Ji; Xiangyu Jin; Shuling Wang 003; Naijun Zhan (CoRR, 2024)

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes. - Xiangyu Jin; Bohua Zhan; Shuling Wang 003; Naijun Zhan (CoRR, 2024)

Case Study: Modeling, Simulation, Verification, and Code Generation of an Automatic Cruise Control System. - Xiong Xu; Shuling Wang 003; Zekun Ji; Qiang Gao; Xiangyu Jin; Bohua Zhan; Naijun Zhan (The Practice of Formal Methods (II), 2024)

HpC: A Calculus for Hybrid and Mobile Systems. - Xiong Xu; Jean-Pierre Talpin; Shuling Wang 003; Hao Wu 085; Bohua Zhan; Xinxin Liu; Naijun Zhan (Proc. ACM Program. Lang., 2025)

HpC: A Calculus for Hybrid and Mobile Systems - Full Version. - Xiong Xu; Jean-Pierre Talpin; Shuling Wang 003; Hao Wu 085; Bohua Zhan; Xinxin Liu; Naijun Zhan (CoRR, 2025)

Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries. - Fanpeng Yang; Xu Ma; Shuling Wang 003; Xiong Xu; Qinxiang Cao; Naijun Zhan; Xiaofeng Li; Bin Gu 006 (CoRR, 2025)