Naijun Zhan

ORCID

Publication Activity (10 Years)

Years Active: 1999-2024
Publications (10 Years): 105

Top Venues

CoRR

IEEE Trans. Autom. Control.

ATVA

SETTA

Publications

Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang, Wanwei Liu
Reach-Avoid Verification Based on Convex Optimization. IEEE Trans. Autom. Control. 69 (1) (2024)
Han Su, Shenghua Feng, Sinong Zhan, Naijun Zhan
Switching Controller Synthesis for Hybrid Systems Against STL Formulas. CoRR (2024)
Bai Xue, Naijun Zhan, Martin Fränzle
Reach-Avoid Analysis for Polynomial Stochastic Differential Equations. IEEE Trans. Autom. Control. 69 (3) (2024)
Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes. CoRR (2024)
Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, Naijun Zhan
A decision procedure for string constraints with string/integer conversion and flat regular constraints. Acta Informatica 61 (1) (2024)
Shuling Wang, Zekun Ji, Xiong Xu, Bohua Zhan, Qiang Gao, Naijun Zhan
Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. ICCPS (2024)
Tengshun Yang, Hongfei Fu, Jingyu Ke, Naijun Zhan, Shiyang Wu
Piecewise Linear Expectation Analysis via k-Induction for Probabilistic Programs. CoRR (2024)
Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, Naijun Zhan
Formally Verified C Code Generation from Hybrid Communicating Sequential Processes. CoRR (2024)
Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan
Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets. CoRR (2024)
Bohua Zhan, Xiong Xu, Qiang Gao, Zekun Ji, Xiangyu Jin, Shuling Wang, Naijun Zhan
Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems. CoRR (2024)
Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan
Generalizing SDP-Based Barrier Certificate Synthesis to Unbounded Domains by Dropping Archimedean Condition. CoRR (2023)
Xiong Xu, Bohua Zhan, Shuling Wang, Jean-Pierre Talpin, Naijun Zhan
A denotational semantics of Simulink with higher-order UTP. J. Log. Algebraic Methods Program. 130 (2023)
Marieke Huisman, Corina S. Pasareanu, Naijun Zhan
Introduction to the Special Section on FM 2021. Formal Aspects Comput. 35 (2) (2023)
Wenyou Liu, Yunjun Bai, Li Jiao, Naijun Zhan
Safety guarantee for time-delay systems with disturbances. Sci. China Inf. Sci. 66 (3) (2023)
Jiang Liu, Han Su, Yunjun Bai, Bin Gu, Bai Xue, Mengfei Yang, Naijun Zhan
Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller. CoRR (2023)
Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan
Semantics Foundation for Cyber-physical Systems Using Higher-order UTP. ACM Trans. Softw. Eng. Methodol. 32 (1) (2023)
Han Su, Jiyu Zhu, Shenghua Feng, Yunjun Bai, Bin Gu, Jiang Liu, Mengfei Yang, Naijun Zhan
Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems. CoRR (2023)
Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi, Zhi-Hong Yang
Synthesizing Invariants for Polynomial Programs by Semidefinite Programming. CoRR (2023)
Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan
Lower Bounds for Possibly Divergent Probabilistic Programs. Proc. ACM Program. Lang. 7 (OOPSLA1) (2023)
Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan
Lower Bounds for Possibly Divergent Probabilistic Programs. CoRR (2023)
Naijun Zhan, Bohua Zhan, Shuling Wang, Dimitar P. Guelev, Xiangyu Jin
A Generalized Hybrid Hoare Logic. CoRR (2023)
Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan
Machine-Checked Executable Semantics of Stateflow. ICFEM (2022)
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming. Inf. Comput. 289 (Part) (2022)
Bai Xue, Naijun Zhan
Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems. IEEE Trans. Autom. Control. 67 (2) (2022)
Depeng Liu, Lutan Zhao, Pengfei Yang, Bow-Yaw Wang, Rui Hou, Lijun Zhang, Naijun Zhan
Defensive Design of Saturating Counters Based on Differential Privacy. CoRR (2022)
Marieke Huisman, Corina S. Pasareanu, Naijun Zhan
Preface for the formal methods in system design special issue on 'Formal Methods 2021'. Formal Methods Syst. Des. 61 (1) (2022)
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming. CoRR (2022)
Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan
Machine-checked executable semantics of Stateflow. CoRR (2022)
Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan
Learning Deterministic One-Clock Timed Automata via Mutation Testing. ATVA (2022)
Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao
Formal Analysis of 5G Authentication and Key Management for Applications (AKMA). J. Syst. Archit. 126 (2022)
Bai Xue, Naijun Zhan, Martin Fränzle
Reach-Avoid Analysis for Stochastic Differential Equations. CoRR (2022)
Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle, Shenghua Feng
Differential Games Based on Invariant Sets Generation. ACC (2022)
Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan
Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow. Theor. Comput. Sci. 903 (2022)
Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang, Wanwei Liu
Reach-avoid Verification Based on Convex Optimization. CoRR (2022)
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. CoRR (2021)
Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan
Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control. Acta Informatica 58 (5) (2021)
Arvind Easwaran, Qi Zhu, Naijun Zhan
Special issue on design of embedded software and systems (SI: ICESS19). J. Syst. Archit. 116 (2021)
Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao
Formal Analysis of 5G AKMA. SETTA (2021)
Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang, Naijun Zhan
Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. RTAS (2021)
Stefan Mitsch, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving. ARCH@ADHS (2021)
Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue, Naijun Zhan
Switching controller synthesis for delay hybrid systems under perturbations. HSCC (2021)
Bai Xue, Renjue Li, Naijun Zhan, Martin Fränzle
Reach-avoid Analysis for Stochastic Discrete-time Systems. ACC (2021)
Bai Xue, Qiuye Wang, Shenghua Feng, Naijun Zhan
Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations. IEEE Trans. Autom. Control. 66 (1) (2021)
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. CAV (1) (2021)
Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Inferring Switched Nonlinear Dynamical Systems. Formal Aspects Comput. 33 (3) (2021)
Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang, Zhikun She
Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. SIAM J. Control. Optim. 59 (2) (2021)
Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning real-time automata. Sci. China Inf. Sci. 64 (9) (2021)
Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue, Naijun Zhan
Switching Controller Synthesis for Delay Hybrid Systems under Perturbations. CoRR (2021)
Bai Xue, Yunjun Bai, Naijun Zhan, Wenyou Liu, Li Jiao
Reach-Avoid Analysis for Delay Differential Equations. CDC (2021)
Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning Nondeterministic Real-Time Automata. ACM Trans. Embed. Comput. Syst. 20 (5s) (2021)
Gaogao Yan, Li Jiao, Shuling Wang, Lingtai Wang, Naijun Zhan
Automatically Generating SystemC Code from HCSP Formal Models. ACM Trans. Softw. Eng. Methodol. 29 (1) (2020)
Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan
Unbounded-Time Safety Verification of Stochastic Differential Dynamics. CAV (2) (2020)
Bai Xue, Martin Fränzle, Naijun Zhan
Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties. IEEE Trans. Autom. Control. 65 (4) (2020)
Bai Xue, Naijun Zhan, Martin Fränzle
Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems. CDC (2020)
Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, Liyun Dai
Nonlinear Craig Interpolant Generation. CAV (1) (2020)
Bai Xue, Naijun Zhan
Probably Approximately Correct Interpolants Generation. SETTA (2020)
Stefan Mitsch, Jonathan Julián Huerta y Munive, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving. ARCH (2020)
Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan
PAC Learning of Deterministic One-Clock Timed Automata. ICFEM (2020)
Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, Ting Gan
From model to implementation: a network algorithm programming language. Sci. China Inf. Sci. 63 (7) (2020)
Bai Xue, Martin Fränzle, Naijun Zhan, Sergiy Bogomolov, Bican Xia
Safety Verification for Random Ordinary Differential Equations. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39 (11) (2020)
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning One-Clock Timed Automata. TACAS (1) (2020)
Ting Gan, Bican Xia, Bai Xue, Naijun Zhan
Nonlinear Craig Interpolant Generation. CoRR (2019)
Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle
Robust invariant sets generation for state-constrained perturbed polynomial systems. HSCC (2019)
Qiuye Wang, Lihong Zhi, Naijun Zhan, Bai Xue, Zhi-Hong Yang
Synthesizing More Expressive Invariants by Semidefinite Programming. CoRR (2019)
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning One-Clock Timed Automata. CoRR (2019)
Martin Fränzle, Deepak Kapur, Heike Wehrheim, Naijun Zhan
Editorial. Formal Aspects Comput. 31 (1) (2019)
Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan
ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving. ARCH@CPSIoTWeek (2019)
Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan
NIL: Learning Nonlinear Interpolants. CoRR (2019)
Bai Xue, Martin Fränzle, Hengjun Zhao, Naijun Zhan, Arvind Easwaran
Probably Approximate Safety Verification of Hybrid Dynamical Systems. ICFEM (2019)
Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan
NIL: Learning Nonlinear Interpolants. CADE (2019)
Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, Bai Xue
Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations. CAV (1) (2019)
Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. CAV (2) (2019)
Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan
Quantum Hoare Logic. Arch. Formal Proofs 2019 (2019)
Haolan Zhan, Qianqian Lin, Shuling Wang, Jean-Pierre Talpin, Xiong Xu, Naijun Zhan
Unified Graphical Co-modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow. UTP (2019)
Bai Xue, Naijun Zhan, Yangjia Li, Qiuye Wang
Robust Non-termination Analysis of Numerical Software. SETTA (2018)
Liyun Dai, Taolue Chen, Zhiming Liu, Bican Xia, Naijun Zhan, Kim G. Larsen
Parameter Synthesis Problems for one parametric clock Timed Automata. CoRR (2018)
Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan
ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving. ARCH@ADHS (2018)
Bai Xue, Martin Fränzle, Naijun Zhan
Under-Approximating Reach Sets for Polynomial Continuous Systems. HSCC (2018)
Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang, Zhikun She
Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. CoRR (2018)
Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan
Monitoring CTMCs by Multi-clock Timed Automata. CAV (1) (2018)
Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang, Wang Yi
Model Checking Bounded Continuous-time Extended Linear Duration Invariants. HSCC (2018)
Bai Xue, Naijun Zhan
Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems. CoRR (2018)
Lingtai Wang, Naijun Zhan, Jie An
The Opacity of Real-Time Automata. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37 (11) (2018)
Bai Xue, Qiuye Wang, Shenghua Feng, Naijun Zhan
Over- and Under-Approximating Reachable Sets for Perturbed Delay Differential Equations. CoRR (2018)
Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, Naijun Zhan
Reachability Analysis for Solvable Dynamical Systems. IEEE Trans. Autom. Control. 63 (7) (2018)
Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan
What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed Interaction. ATVA (2018)
Dimitar P. Guelev, Shuling Wang, Naijun Zhan
Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus. CoRR (2017)
Qiuye Wang, Yangjia Li, Bican Xia, Naijun Zhan
Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems. J. Syst. Sci. Complex. 30 (1) (2017)
Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia
Finding Polynomial Loop Invariants for Probabilistic Programs. ATVA (2017)
Bai Xue, Peter Nazier Mosaad, Martin Fränzle, Mingshuai Chen, Yangjia Li, Naijun Zhan
Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations. FORMATS (2017)
Liyun Dai, Ting Gan, Bican Xia, Naijun Zhan
Barrier certificates revisited. J. Symb. Comput. 80 (2017)
Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan
Synthesizing SystemC Code from Delay Hybrid CSP. APLAS (2017)
Shuling Wang, Naijun Zhan, Lijun Zhang
A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. Formal Aspects Comput. 29 (4) (2017)
Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan
Synthesizing SystemC Code from Delay Hybrid CSP. CoRR (2017)
Dimitar P. Guelev, Shuling Wang, Naijun Zhan
Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus. SETTA (2017)
Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia
Finding polynomial loop invariants for probabilistic programs. CoRR (2017)
Shuling Wang, Flemming Nielson, Hanne Riis Nielson, Naijun Zhan
Modelling and Verifying Communication Failure of Hybrid Systems in HCSP. Comput. J. 60 (8) (2017)
Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, Naijun Zhan
A Theorem Prover for Quantum Hoare Logic and Its Applications. CoRR (2016)
Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan
Validated Simulation-Based Verification of Delayed Differential Dynamics. FM (2016)
Mingshuai Chen, Anders P. Ravn, Shuling Wang, Mengfei Yang, Naijun Zhan
A Two-Way Path Between Formal and Informal Design of Embedded Systems. UTP (2016)

Naijun Zhan.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Naijun Zhan