A Formal Proof of the Rate Monotonic Scheduler. - Shuzhen Dong; Qiwen Xu; Naijun Zhan (RTCSA, 1999)

Completeness of Higher-Order Duration Calculus. - Naijun Zhan (CSL, 2000)

Another formal proof for Deadline Driven Scheduler. - Naijun Zhan (RTCSA, 2000)

Automatic Synthesis of the DC Specifications of Lip Synchronisation Protocol. - Huadong Ma; Liang Li; Jianzhong Wang; Naijun Zhan (APSEC, 2001)

An Intuitive Formal Proof for Deadline Driven Scheduler. - Naijun Zhan (J. Comput. Sci. Technol., 2001)

Combining Hierarchical Specification with Hierarchical Implementation. - Naijun Zhan (ASIAN, 2003)

Action Refinement from a Logical Point of View. - Mila E. Majster-Cederbaum; Naijun Zhan; Harald Fecher (VMCAI, 2003)

Compositional Properties of Sequential Processes. - Naijun Zhan (SVV@ICLP, 2003)

Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity. - Mila E. Majster-Cederbaum; Jinzhao Wu; Houguang Yue; Naijun Zhan (ICFEM, 2004)

Deriving Non-determinism from Conjunction and Disjunction. - Naijun Zhan; Mila E. Majster-Cederbaum (FORTE, 2005)

Compositionality of Fixpoint Logic with Chop. - Naijun Zhan; Jinzhao Wu (ICTAC, 2005)

Program Verification by Using DISCOVERER. - Lu Yang; Naijun Zhan; Bican Xia; Chaochen Zhou (VSTTE, 2005)

Connecting Algebraic and Logical Descriptions of Concurrent Systems. - Naijun Zhan (ISoLA, 2006)

Generating Polynomial Invariants with DISCOVERER and QEPCAD. - Yinghua Chen; Bican Xia; Lu Yang; Naijun Zhan (Formal Methods and Hybrid Real-Time Systems, 2007)

Modelling with Relational Calculus of Object and Component Systems - rCOS. - Zhenbang Chen; Abdelhakim Hannousse; Dang Van Hung; Istvan Knoll; Xiaoshan Li; Zhiming Liu 001; Yang Liu; Qu Nan; Joseph C. Okika; Anders P. Ravn; Volker Stolz; Lu Yang; et al. (CoCoME, 2007)

A Model of Component-Based Programming. - Xin Chen 027; Jifeng He 001; Zhiming Liu 001; Naijun Zhan (FSEN, 2007)

Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. - Yinghua Chen; Bican Xia; Lu Yang; Naijun Zhan; Chaochen Zhou (ICTAC, 2007)

Program Verification by Reduction to Semi-algebraic Systems Solving. - Bican Xia; Lu Yang; Naijun Zhan (ISoLA, 2008)

Component Publications and Compositions. - Naijun Zhan; Eun-Young Kang 001; Zhiming Liu 001 (UTP, 2008)

Basic research in computer science and software engineering at SKLCS. - Jian Zhang 001; Wenhui Zhang; Naijun Zhan; Yi-Dong Shen; Haiming Chen 001; Yunquan Zhang; Yongji Wang; Enhua Wu; Hongan Wang; Xueyang Zhu (Frontiers Comput. Sci. China, 2008)

Formalising Scheduling Theories in Duration Calculus. - Qiwen Xu; Naijun Zhan (Nord. J. Comput., 2008)

Model Checking Linear Duration Invariants of Networks of Automata. - Miaomiao Zhang 003; Zhiming Liu 001; Naijun Zhan (FSEN, 2009)

Refinement and verification in component-based model-driven design. - Zhenbang Chen; Zhiming Liu 001; Anders P. Ravn; Volker Stolz; Naijun Zhan (Sci. Comput. Program., 2009)

A Calculus for Hybrid CSP. - Jiang Liu 009; Jidong Lv; Zhao Quan; Naijun Zhan; Hengjun Zhao; Chaochen Zhou; Liang Zou (APLAS, 2010)

Refinement of models of software components. - Zizhen Wang; Hanpin Wang; Naijun Zhan (SAC, 2010)

Recent advances in program verification through computer algebra. - Lu Yang; Chaochen Zhou; Naijun Zhan; Bican Xia (Frontiers Comput. Sci. China, 2010)

On hierarchically developing reactive systems. - Naijun Zhan; Mila E. Majster-Cederbaum (Inf. Comput., 2010)

Rate monotonic scheduling re-analysed. - Qiwen Xu; Naijun Zhan (Inf. Process. Lett., 2010)

Connection between logical and algebraic approaches to concurrent systems. - Naijun Zhan (Math. Struct. Comput. Sci., 2010)

Computing semi-algebraic invariants for polynomial dynamical systems. - Jiang Liu 009; Naijun Zhan; Hengjun Zhao (EMSOFT, 2011)

A Complete Method to Polynomial Differential Invariant Generation for Hybrid Systems - Jiang Liu 009; Naijun Zhan; Hengjun Zhao (CoRR, 2011)

Symbolic decision procedure for termination of linear programs. - Bican Xia; Lu Yang; Naijun Zhan; Zhihai Zhang (Formal Aspects Comput., 2011)

Unblockable compositions of software components. - Ruzhen Dong; Johannes Faber; Zhiming Liu 001; Jirí Srba; Naijun Zhan; Jiaqi Zhu 001 (CBSE, 2012)

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example. - Hengjun Zhao; Naijun Zhan; Deepak Kapur; Kim G. Larsen (FM, 2012)

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

Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems. - Jiang Liu 009; Naijun Zhan; Hengjun Zhao (Math. Comput. Sci., 2012)

CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains. - Yang Gao; Ernst Moritz Hahn; Naijun Zhan; Lijun Zhang 001 (ATVA, 2013)

Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants. - Hengjun Zhao; Naijun Zhan; Deepak Kapur (Theories of Programming and Formal Methods, 2013)

Generating Non-linear Interpolants by Semidefinite Programming. - Liyun Dai; Bican Xia; Naijun Zhan (CAV, 2013)

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

Towards a Failure Model of Software Components. - Ruzhen Dong; Naijun Zhan (FACS, 2013)

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

Bounded model-checking of discrete duration calculus. - Quan Zu; Miaomiao Zhang 003; Jiaqi Zhu 001; Naijun Zhan (HSCC, 2013)

An Interface Model of Software Components. - Ruzhen Dong; Naijun Zhan; Liang Zhao 021 (ICTAC, 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)

Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation - Deepak Kapur; Naijun Zhan; Hengjun Zhao (CoRR, 2013)

Model checking conditional CSL for continuous-time Markov chains. - Yang Gao; Ming Xu 010; Naijun Zhan; Lijun Zhang 001 (Inf. Process. Lett., 2013)

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

Formal Verification of a Descent Guidance Control Program of a Lunar Lander. - Hengjun Zhao; Mengfei Yang; Naijun Zhan; Bin Gu 006; Liang Zou; Yao Chen (FM, 2014)

Combining Formal and Informal Methods in the Design of Spacecrafts. - Mengfei Yang; Naijun Zhan (SETSS, 2014)

Hybrid annex: an AADL extension for continuous behavior and cyber-physical interaction modeling. - Ehsan Ahmad; Brian R. Larson; Stephen C. Barrett; Naijun Zhan; Yunwei Dong (HILT, 2014)

Discovering non-terminating inputs for multi-path polynomial programs. - Jiang Liu 009; Ming Xu 010; Naijun Zhan; Hengjun Zhao (J. Syst. Sci. Complex., 2014)

Decidability of the Reachability for a Family of Linear Vector Fields. - Ting Gan; Mingshuai Chen; Liyun Dai; Bican Xia; Naijun Zhan (ATVA, 2015)

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

Automatic Verification of Stability and Safety for Delay Differential Equations. - Liang Zou; Martin Fränzle; Naijun Zhan; Peter Nazier Mosaad (CAV (2), 2015)

Abstraction of Elementary Hybrid Systems by Variable Transformation. - Jiang Liu 009; Naijun Zhan; Hengjun Zhao; Liang Zou (FM, 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)

Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL. - Ehsan Ahmad; Yunwei Dong; Brian R. Larson; Jidong Lü; Tao Tang 004; Naijun Zhan (Sci. China Inf. Sci., 2015)

Termination Analysis of Polynomial Programs with Equality Conditions. - Yangjia Li; Hui Lu; Naijun Zhan; Mingshuai Chen; Guohua Wu (CoRR, 2015)

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. - Ting Gan; Liyun Dai; Bican Xia; Naijun Zhan; Deepak Kapur; Mingshuai Chen (IJCAR, 2016)

Computing reachable sets of linear vector fields revisited. - Ting Gan; Mingshuai Chen; Yangjia Li; Bican Xia; Naijun Zhan (ECC, 2016)

Validated Simulation-Based Verification of Delayed Differential Dynamics. - Mingshuai Chen; Martin Fränzle; Yangjia Li; Peter Nazier Mosaad; Naijun Zhan (FM, 2016)

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)

Interpolation synthesis for quadratic polynomial inequalities and combination with textit{EUF}. - Ting Gan; Liyun Dai; Bican Xia; Naijun Zhan; Deepak Kapur; Mingshuai Chen (CoRR, 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)

Finding Polynomial Loop Invariants for Probabilistic Programs. - Yijun Feng; Lijun Zhang 001; David N. Jansen; Naijun Zhan; Bican Xia (ATVA, 2017)

Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations. - Bai Xue 001; Peter Nazier Mosaad; Martin Fränzle; Mingshuai Chen; Yangjia Li; Naijun Zhan (FORMATS, 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)

Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems. - Qiuye Wang; Yangjia Li; Bican Xia; Naijun Zhan (J. Syst. Sci. Complex., 2017)

Barrier certificates revisited. - Liyun Dai; Ting Gan; Bican Xia; Naijun Zhan (J. Symb. 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)

What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed Interaction. - Mingshuai Chen; Martin Fränzle; Yangjia Li; Peter Nazier Mosaad; Naijun Zhan (ATVA, 2018)

Decidability of the Initial-State Opacity of Real-Time Automata. - Lingtai Wang; Naijun Zhan (Symposium on Real-Time and Hybrid Systems, 2018)

Monitoring CTMCs by Multi-clock Timed Automata. - Yijun Feng; Joost-Pieter Katoen; Haokun Li; Bican Xia; Naijun Zhan (CAV (1), 2018)

Under-Approximating Reach Sets for Polynomial Continuous Systems. - Bai Xue 001; Martin Fränzle; Naijun Zhan (HSCC, 2018)

Model Checking Bounded Continuous-time Extended Linear Duration Invariants. - Jie An 001; Naijun Zhan; Xiaoshan Li; Miaomiao Zhang 003; Wang Yi 001 (HSCC, 2018)

Robust Non-termination Analysis of Numerical Software. - Bai Xue 001; Naijun Zhan; Yangjia Li; Qiuye Wang (SETTA, 2018)

Parameter Synthesis Problems for one parametric clock Timed Automata. - Liyun Dai; Taolue Chen 001; Zhiming Liu 001; Bican Xia; Naijun Zhan; Kim G. Larsen (CoRR, 2018)

Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems. - Bai Xue 001; Naijun Zhan (CoRR, 2018)

Over- and Under-Approximating Reachable Sets for Perturbed Delay Differential Equations. - Bai Xue 001; Qiuye Wang; Shenghua Feng; Naijun Zhan (CoRR, 2018)

Reachability Analysis for Solvable Dynamical Systems. - Ting Gan; Mingshuai Chen; Yangjia Li; Bican Xia; Naijun Zhan (IEEE Trans. Autom. Control., 2018)

The Opacity of Real-Time Automata. - Lingtai Wang; Naijun Zhan; Jie An 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018)

NIL: Learning Nonlinear Interpolants. - Mingshuai Chen; Jian Wang 042; Jie An 001; Bohua Zhan; Deepak Kapur; Naijun Zhan (CADE, 2019)

Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations. - Shenghua Feng; Mingshuai Chen; Naijun Zhan; Martin Fränzle; Bai Xue 001 (CAV (1), 2019)

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)

Robust invariant sets generation for state-constrained perturbed polynomial systems. - Bai Xue 001; Qiuye Wang; Naijun Zhan; Martin Fränzle (HSCC, 2019)

Probably Approximate Safety Verification of Hybrid Dynamical Systems. - Bai Xue 001; Martin Fränzle; Hengjun Zhao; Naijun Zhan; Arvind Easwaran (ICFEM, 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)

Nonlinear Craig Interpolant Generation. - Ting Gan; Bican Xia; Bai Xue 001; Naijun Zhan (CoRR, 2019)

Synthesizing More Expressive Invariants by Semidefinite Programming. - Qiuye Wang; Lihong Zhi; Naijun Zhan; Bai Xue 001; Zhi-Hong Yang (CoRR, 2019)

Editorial. - Martin Fränzle; Deepak Kapur; Heike Wehrheim; Naijun Zhan (Formal Aspects Comput., 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)

Unbounded-Time Safety Verification of Stochastic Differential Dynamics. - Shenghua Feng; Mingshuai Chen; Bai Xue 001; Sriram Sankaranarayanan 001; Naijun Zhan (CAV (2), 2020)

Nonlinear Craig Interpolant Generation. - Ting Gan; Bican Xia; Bai Xue 001; Naijun Zhan; Liyun Dai (CAV (1), 2020)

Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems. - Bai Xue 001; Naijun Zhan; Martin Fränzle (CDC, 2020)

PAC Learning of Deterministic One-Clock Timed Automata. - Wei Shen; Jie An 001; Bohua Zhan; Miaomiao Zhang 003; Bai Xue 001; Naijun Zhan (ICFEM, 2020)

Probably Approximately Correct Interpolants Generation. - Bai Xue 001; Naijun Zhan (SETTA, 2020)

Learning One-Clock Timed Automata. - Jie An 001; Mingshuai Chen; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (TACAS (1), 2020)

From model to implementation: a network algorithm programming language. - Jian Wang 042; Jie An 001; Mingshuai Chen; Naijun Zhan; Lulin Wang; Miaomiao Zhang 003; Ting Gan (Sci. China Inf. Sci., 2020)

Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties. - Bai Xue 001; Martin Fränzle; Naijun Zhan (IEEE Trans. Autom. Control., 2020)

Safety Verification for Random Ordinary Differential Equations. - Bai Xue 001; Martin Fränzle; Naijun Zhan; Sergiy Bogomolov; Bican Xia (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 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)

Reach-avoid Analysis for Stochastic Discrete-time Systems. - Bai Xue 001; Renjue Li; Naijun Zhan; Martin Fränzle (ACC, 2021)

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

Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. - Qiuye Wang; Mingshuai Chen; Bai Xue 001; Naijun Zhan; Joost-Pieter Katoen (CAV (1), 2021)

Reach-Avoid Analysis for Delay Differential Equations. - Bai Xue 001; Yunjun Bai; Naijun Zhan; Wenyou Liu; Li Jiao (CDC, 2021)

Switching controller synthesis for delay hybrid systems under perturbations. - Yunjun Bai; Ting Gan; Li Jiao; Bican Xia; Bai Xue 001; Naijun Zhan (HSCC, 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)

Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control. - Mingshuai Chen; Martin Fränzle; Yangjia Li; Peter Nazier Mosaad; Naijun Zhan (Acta Informatica, 2021)

Learning real-time automata. - Jie An 001; Lingtai Wang; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (Sci. China Inf. Sci., 2021)

Inferring Switched Nonlinear Dynamical Systems. - Xiangyu Jin; Jie An 001; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (Formal Aspects Comput., 2021)

Special issue on design of embedded software and systems (SI: ICESS19). - Arvind Easwaran; Qi Zhu; Naijun Zhan (J. Syst. Archit., 2021)

Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. - Bai Xue 001; Qiuye Wang; Naijun Zhan; Shijie Wang; Zhikun She (SIAM J. Control. Optim., 2021)

Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations. - Bai Xue 001; Qiuye Wang; Shenghua Feng; Naijun Zhan (IEEE Trans. Autom. Control., 2021)

Learning Nondeterministic Real-Time Automata. - Jie An 001; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (ACM Trans. Embed. Comput. Syst., 2021)

Differential Games Based on Invariant Sets Generation. - Bai Xue 001; Qiuye Wang; Naijun Zhan; Martin Fränzle; Shenghua Feng (ACC, 2022)

Learning Deterministic One-Clock Timed Automata via Mutation Testing. - Xiaochen Tang; Wei Shen; Miaomiao Zhang 003; Jie An 001; Bohua Zhan; Naijun Zhan (ATVA, 2022)

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

Defensive Design of Saturating Counters Based on Differential Privacy. - Depeng Liu; Lutan Zhao; Pengfei Yang 002; Bow-Yaw Wang; Rui Hou 001; Lijun Zhang 001; Naijun Zhan (CoRR, 2022)

Reach-Avoid Analysis for Stochastic Differential Equations. - Bai Xue 001; Naijun Zhan; Martin Fränzle (CoRR, 2022)

Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming. - Qiuye Wang; Mingshuai Chen; Bai Xue 001; Naijun Zhan; Joost-Pieter Katoen (Inf. Comput., 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)

Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems. - Bai Xue 001; Naijun Zhan (IEEE Trans. Autom. Control., 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)

Preface for the formal methods in system design special issue on 'Formal Methods 2021'. - Marieke Huisman; Corina S. Pasareanu; Naijun Zhan (Formal Methods Syst. Des., 2022)

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

Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller. - Jiang Liu 009; Han Su 003; Yunjun Bai; Bin Gu 006; Bai Xue 001; Mengfei Yang; Naijun Zhan (CoRR, 2023)

Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems. - Han Su 003; Jiyu Zhu; Shenghua Feng; Yunjun Bai; Bin Gu 006; Jiang Liu 009; Mengfei Yang; Naijun Zhan (CoRR, 2023)

Generalizing SDP-Based Barrier Certificate Synthesis to Unbounded Domains by Dropping Archimedean Condition. - Hao Wu 085; Shenghua Feng; Ting Gan; Jie Wang 037; Bican Xia; Naijun Zhan (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)

Safety guarantee for time-delay systems with disturbances. - Wenyou Liu; Yunjun Bai; Li Jiao; Naijun Zhan (Sci. China Inf. Sci., 2023)

Lower Bounds for Possibly Divergent Probabilistic Programs. - Shenghua Feng; Mingshuai Chen; Han Su 003; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Naijun Zhan (Proc. ACM Program. Lang., 2023)

Introduction to the Special Section on FM 2021. - Marieke Huisman; Corina S. Pasareanu; Naijun Zhan (Formal Aspects Comput., 2023)

A Unified Framework for Quantitative Analysis of Probabilistic Programs. - Shenghua Feng; Tengshun Yang; Mingshuai Chen; Naijun Zhan (Principles of Verification (1), 2024)

The Opacity of Timed Automata. - Jie An 001; Qiang Gao; Lingtai Wang; Naijun Zhan; Ichiro Hasuo (FM (1), 2024)

Switching Controller Synthesis for Hybrid Systems Against STL Formulas. - Han Su 003; Shenghua Feng; Sinong Zhan; Naijun Zhan (FM (2), 2024)

On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains. - Hao Wu 085; Shenghua Feng; Ting Gan; Jie Wang 037; Bican Xia; Naijun Zhan (FM (2), 2024)

Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets. - Hao Wu 085; Jie Wang 037; Bican Xia; Xiakun Li; Naijun Zhan; Ting Gan (FM (1), 2024)

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)

Improving the Reaction Latency Analysis of Message Synchronization in ROS. - Chenhao Wu; Ruoxiang Li; Naijun Zhan; Nan Guan (RTCSA, 2024)

Cache Behavior Analysis with SP-Relative Addressing for WCET Estimation. - Shangshang Xiao; Mengxia Sun; Wei Zhang 173; Naijun Zhan; Lei Ju 001 (SETTA, 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)

Piecewise Linear Expectation Analysis via k-Induction for Probabilistic Programs. - Tengshun Yang; Hongfei Fu 001; Jingyu Ke; Naijun Zhan; Shiyang Wu (CoRR, 2024)

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

Preface to the Special Issue on Formal Methods and Applications. - Qinxiang Cao; Fu Song; Naijun Zhan (Int. J. Softw. Informatics, 2024)

Reset controller synthesis: a correct-by-construction way to the design of CPS. - Naijun Zhan; Han Su 003; Mengfei Yang; Bin Gu 006 (Res. Dir. Cyber Phys. Syst., 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)

Reach-Avoid Verification Based on Convex Optimization. - Bai Xue 001; Naijun Zhan; Martin Fränzle; Ji Wang 001; Wanwei Liu (IEEE Trans. Autom. Control., 2024)

A decision procedure for string constraints with string/integer conversion and flat regular constraints. - Hao Wu 085; Yu-Fang Chen 001; Zhilin Wu; Bican Xia; Naijun Zhan (Acta Informatica, 2024)

Reach-Avoid Analysis for Polynomial Stochastic Differential Equations. - Bai Xue 001; Naijun Zhan; Martin Fränzle (IEEE Trans. Autom. Control., 2024)

Modeling and Analysis of the LatestTime Message Synchronization Policy in ROS. - Chenhao Wu; Ruoxiang Li; Naijun Zhan; Nan Guan (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2024)

Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge. - Yue Fang; Zhi Jin; Jie An 001; Hongshen Chen; Xiaohong Chen; Naijun Zhan (ACL (Findings), 2025)

Runtime Enforcement of CPS against Signal Temporal Logic. - Han Su 003; Saumya Shankar; Srinivas Pinisetty; Partha S. Roop; Naijun Zhan (HSCC, 2025)

Learning Subject to Constraints via Abstract Gradient Descent. - Shiwen Yu; Wanwei Liu; Zengyu Liu; Liqian Chen; Ting Wang 009; Naijun Zhan; Ji Wang 001 (NeuS, 2025)

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)

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming. - Hao Wu 085; Qiuye Wang; Bai Xue 001; Naijun Zhan; Lihong Zhi; Zhi-Hong Yang (ACM Trans. Program. Lang. Syst., 2025)

NEAT: QCP: A Practical Separation Logic-based C Program Verification Tool. - Xiwei Wu; Yueyang Feng; Xiaoyang Lu; Tianchuan Lin; Kan Liu; Zhiyi Wang; Shushu Wu; Lihan Xie; Chengxi Yang; Hongyi Zhong; Naijun Zhan; Zhenjiang Hu; et al. (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)

WCET Estimation for CNN Inference on FPGA SoC With Multi-DPU Engines. - Wei Zhang 173; Yunlong Yu; Xiao Jiang; Nan Guan; Naijun Zhan; Lei Ju 001 (IEEE Trans. Parallel Distributed Syst., 2025)

Derivative-Agnostic Inference of Nonlinear Hybrid Systems. - Hengzhi Yu; Bohan Ma; Mingshuai Chen; Jie An 001; Bin Gu 006; Naijun Zhan; Jianwei Yin (CoRR, 2025)