Naijun Zhan

According to our database, Naijun Zhan authored at least 160 papers between 1999 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

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., November, 2024

Reach-Avoid Analysis for Polynomial Stochastic Differential Equations.

Bai Xue, Naijun Zhan, Martin Fränzle

IEEE Trans. Autom. Control., March, 2024

A decision procedure for string constraints with string/integer conversion and flat regular constraints.

Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, Naijun Zhan

Acta Informatica, March, 2024

Reach-Avoid Verification Based on Convex Optimization.

Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang, Wanwei Liu

IEEE Trans. Autom. Control., January, 2024

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes.

Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan

CoRR, 2024

Piecewise Linear Expectation Analysis via k-Induction for Probabilistic Programs.

Tengshun Yang, Hongfei Fu, Jingyu Ke, Naijun Zhan, Shiyang Wu

CoRR, 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, Naijun Zhan

CoRR, 2024

The Design of Intelligent Temperature Control System of Smart House with MARS.

Yihao Yin, Hao Wu, Shuling Wang, Xiong Xu, Fanjiang Xu, Naijun Zhan

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2024

Cache Behavior Analysis with SP-Relative Addressing for WCET Estimation.

Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, Lei Ju

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2024

Improving the Reaction Latency Analysis of Message Synchronization in ROS.

Chenhao Wu, Ruoxiang Li, Naijun Zhan, Nan Guan

Proceedings of the 30th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, 2024

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes.

Shuling Wang, Zekun Ji, Xiong Xu, Bohua Zhan, Qiang Gao, Naijun Zhan

Proceedings of the 15th ACM/IEEE International Conference on Cyber-Physical Systems, 2024

Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets.

Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan

Proceedings of the Formal Methods - 26th International Symposium, 2024

On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains.

Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan

Proceedings of the Formal Methods - 26th International Symposium, 2024

Switching Controller Synthesis for Hybrid Systems Against STL Formulas.

Han Su, Shenghua Feng, Sinong Zhan, Naijun Zhan

Proceedings of the Formal Methods - 26th International Symposium, 2024

The Opacity of Timed Automata.

Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan, Ichiro Hasuo

Proceedings of the Formal Methods - 26th International Symposium, 2024

2023

Introduction to the Special Section on FM 2021.

Marieke Huisman, Corina S. Pasareanu, Naijun Zhan

Formal Aspects Comput., June, 2023

Lower Bounds for Possibly Divergent Probabilistic Programs.

Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan

Proc. ACM Program. Lang., April, 2023

Safety guarantee for time-delay systems with disturbances.

Wenyou Liu, Yunjun Bai, Li Jiao, Naijun Zhan

Sci. China Inf. Sci., March, 2023

Semantics Foundation for Cyber-physical Systems Using Higher-order UTP.

Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan

ACM Trans. Softw. Eng. Methodol., January, 2023

A denotational semantics of Simulink with higher-order UTP.

Xiong Xu, Bohua Zhan, Shuling Wang, Jean-Pierre Talpin, Naijun Zhan

J. Log. Algebraic Methods Program., 2023

Generalizing SDP-Based Barrier Certificate Synthesis to Unbounded Domains by Dropping Archimedean Condition.

Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan

CoRR, 2023

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming.

Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi, Zhi-Hong Yang

CoRR, 2023

Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems.

Han Su, Jiyu Zhu, Shenghua Feng, Yunjun Bai, Bin Gu, Jiang Liu, Mengfei Yang, Naijun Zhan

CoRR, 2023

Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller.

Jiang Liu, Han Su, Yunjun Bai, Bin Gu, Bai Xue, Mengfei Yang, Naijun Zhan

CoRR, 2023

A Generalized Hybrid Hoare Logic.

Naijun Zhan, Bohua Zhan, Shuling Wang, Dimitar P. Guelev, Xiangyu Jin

CoRR, 2023

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., August, 2022

Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow.

Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan

Theor. Comput. Sci., 2022

Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems.

Bai Xue, Naijun Zhan

IEEE Trans. Autom. Control., 2022

Formal Analysis of 5G Authentication and Key Management for Applications (AKMA).

Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao

J. Syst. Archit., 2022

Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming.

Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen

Inf. Comput., 2022

Reach-Avoid Analysis for Stochastic Differential Equations.

Bai Xue, Naijun Zhan, Martin Fränzle

CoRR, 2022

Defensive Design of Saturating Counters Based on Differential Privacy.

Depeng Liu, Lutan Zhao, Pengfei Yang, Bow-Yaw Wang, Rui Hou, Lijun Zhang, Naijun Zhan

CoRR, 2022

Machine-Checked Executable Semantics of Stateflow.

Shicheng Yi, Shuling Wang, Bohua Zhan, Naijun Zhan

Proceedings of the Formal Methods and Software Engineering, 2022

Learning Deterministic One-Clock Timed Automata via Mutation Testing.

Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan

Proceedings of the Automated Technology for Verification and Analysis, 2022

Differential Games Based on Invariant Sets Generation.

Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle, Shenghua Feng

Proceedings of the American Control Conference, 2022

2021

Learning Nondeterministic Real-Time Automata.

Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang

ACM Trans. Embed. Comput. Syst., 2021

Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations.

Bai Xue, Qiuye Wang, Shenghua Feng, Naijun Zhan

IEEE Trans. Autom. Control., 2021

Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems.

Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang, Zhikun She

SIAM J. Control. Optim., 2021

Special issue on design of embedded software and systems (SI: ICESS19).

Arvind Easwaran, Qi Zhu, Naijun Zhan

J. Syst. Archit., 2021

Inferring Switched Nonlinear Dynamical Systems.

Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang

Formal Aspects Comput., 2021

Learning real-time automata.

Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang

Sci. China Inf. Sci., 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

Formal Analysis of 5G AKMA.

Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2021

Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander.

Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang, Naijun Zhan

Proceedings of the 27th IEEE Real-Time and Embedded Technology and Applications Symposium, 2021

Switching controller synthesis for delay hybrid systems under perturbations.

Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue, Naijun Zhan

Proceedings of the HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, 2021

Reach-Avoid Analysis for Delay Differential Equations.

Bai Xue, Yunjun Bai, Naijun Zhan, Wenyou Liu, Li Jiao

Proceedings of the 2021 60th IEEE Conference on Decision and Control (CDC), 2021

Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming.

Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving.

Stefan Mitsch, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan

Proceedings of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), 2021

Reach-avoid Analysis for Stochastic Discrete-time Systems.

Bai Xue, Renjue Li, Naijun Zhan, Martin Fränzle

Proceedings of the 2021 American Control Conference, 2021

2020

Automatically Generating SystemC Code from HCSP Formal Models.

Gaogao Yan, Li Jiao, Shuling Wang, Lingtai Wang, Naijun Zhan

ACM Trans. Softw. Eng. Methodol., 2020

Safety Verification for Random Ordinary Differential Equations.

Bai Xue, Martin Fränzle, Naijun Zhan, Sergiy Bogomolov, Bican Xia

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020

Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties.

Bai Xue, Martin Fränzle, Naijun Zhan

IEEE Trans. Autom. Control., 2020

From model to implementation: a network algorithm programming language.

Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, Ting Gan

Sci. China Inf. Sci., 2020

Learning One-Clock Timed Automata.

Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Probably Approximately Correct Interpolants Generation.

Bai Xue, Naijun Zhan

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2020

PAC Learning of Deterministic One-Clock Timed Automata.

Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan

Proceedings of the Formal Methods and Software Engineering, 2020

Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems.

Bai Xue, Naijun Zhan, Martin Fränzle

Proceedings of the 59th IEEE Conference on Decision and Control, 2020

Nonlinear Craig Interpolant Generation.

Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, Liyun Dai

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Unbounded-Time Safety Verification of Stochastic Differential Dynamics.

Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving.

Stefan Mitsch, Jonathan Julián Huerta y Munive, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan

Proceedings of the ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), 2020

2019

Editorial.

Martin Fränzle, Deepak Kapur, Heike Wehrheim, Naijun Zhan

Formal Aspects Comput., 2019

Synthesizing More Expressive Invariants by Semidefinite Programming.

Qiuye Wang, Lihong Zhi, Naijun Zhan, Bai Xue, Zhi-Hong Yang

CoRR, 2019

Nonlinear Craig Interpolant Generation.

Ting Gan, Bican Xia, Bai Xue, Naijun Zhan

CoRR, 2019

Quantum Hoare Logic.

Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan

Arch. Formal Proofs, 2019

Unified Graphical Co-modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow.

Haolan Zhan, Qianqian Lin, Shuling Wang, Jean-Pierre Talpin, Xiong Xu, Naijun Zhan

Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

Probably Approximate Safety Verification of Hybrid Dynamical Systems.

Bai Xue, Martin Fränzle, Hengjun Zhao, Naijun Zhan, Arvind Easwaran

Proceedings of the Formal Methods and Software Engineering, 2019

Robust invariant sets generation for state-constrained perturbed polynomial systems.

Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle

Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019

ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving.

Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan

Proceedings of the ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, 2019

Formal Verification of Quantum Algorithms Using Quantum Hoare Logic.

Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations.

Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, Bai Xue

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

NIL: Learning Nonlinear Interpolants.

Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan

Proceedings of the Automated Deduction - CADE 27, 2019

2018

The Opacity of Real-Time Automata.

Lingtai Wang, Naijun Zhan, Jie An

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018

Reachability Analysis for Solvable Dynamical Systems.

Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, Naijun Zhan

IEEE Trans. Autom. Control., 2018

Over- and Under-Approximating Reachable Sets for Perturbed Delay Differential Equations.

Bai Xue, Qiuye Wang, Shenghua Feng, Naijun Zhan

CoRR, 2018

Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems.

Bai Xue, Naijun Zhan

CoRR, 2018

Parameter Synthesis Problems for one parametric clock Timed Automata.

Liyun Dai, Taolue Chen, Zhiming Liu, Bican Xia, Naijun Zhan, Kim G. Larsen

CoRR, 2018

Robust Non-termination Analysis of Numerical Software.

Bai Xue, Naijun Zhan, Yangjia Li, Qiuye Wang

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2018

Model Checking Bounded Continuous-time Extended Linear Duration Invariants.

Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang, Wang Yi

Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2018

Under-Approximating Reach Sets for Polynomial Continuous Systems.

Bai Xue, Martin Fränzle, Naijun Zhan

Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2018

Monitoring CTMCs by Multi-clock Timed Automata.

Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Decidability of the Initial-State Opacity of Real-Time Automata.

Lingtai Wang, Naijun Zhan

Proceedings of the Symposium on Real-Time and Hybrid Systems, 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

Proceedings of the Automated Technology for Verification and Analysis, 2018

ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving.

Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan

Proceedings of the ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2018

2017

Barrier certificates revisited.

Liyun Dai, Ting Gan, Bican Xia, Naijun Zhan

J. Symb. 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

A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems.

Shuling Wang, Naijun Zhan, Lijun Zhang

Formal Aspects Comput., 2017

Modelling and Verifying Communication Failure of Hybrid Systems in HCSP.

Shuling Wang, Flemming Nielson, Hanne Riis Nielson, Naijun Zhan

Comput. J., 2017

Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus.

Dimitar P. Guelev, Shuling Wang, Naijun Zhan

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2017

Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations.

Bai Xue, Peter Nazier Mosaad, Martin Fränzle, Mingshuai Chen, Yangjia Li, Naijun Zhan

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2017

Finding Polynomial Loop Invariants for Probabilistic Programs.

Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia

Proceedings of the Automated Technology for Verification and Analysis, 2017

Synthesizing SystemC Code from Delay Hybrid CSP.

Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems.

Mingshuai Chen, Xiao Han, Tao Tang, Shuling Wang, Mengfei Yang, Naijun Zhan, Hengjun Zhao, Liang Zou

Proceedings of the Provably Correct Systems, 2017

2016

A Theorem Prover for Quantum Hoare Logic and Its Applications.

Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, Naijun Zhan

CoRR, 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 Two-Way Path Between Formal and Informal Design of Embedded Systems.

Mingshuai Chen, Anders P. Ravn, Shuling Wang, Mengfei Yang, Naijun Zhan

Proceedings of the Unifying Theories of Programming - 6th International Symposium, 2016

Approximate Bisimulation and Discretization of Hybrid CSP.

Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan

Proceedings of the FM 2016: Formal Methods, 2016

Validated Simulation-Based Verification of Delayed Differential Dynamics.

Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan

Proceedings of the FM 2016: Formal Methods, 2016

Computing reachable sets of linear vector fields revisited.

Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, Naijun Zhan

Proceedings of the 15th European Control Conference, 2016

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF.

Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

Termination Analysis of Polynomial Programs with Equality Conditions.

Yangjia Li, Hui Lu, Naijun Zhan, Mingshuai Chen, Guohua Wu

CoRR, 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, Naijun Zhan

Sci. China Inf. Sci., 2015

Extending Hybrid CSP with Probability and Stochasticity.

Yu Peng, Shuling Wang, Naijun Zhan, Lijun Zhang

Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2015

An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems.

Shuling Wang, Naijun Zhan, Liang Zou

Proceedings of the Formal Methods and Software Engineering, 2015

Abstraction of Elementary Hybrid Systems by Variable Transformation.

Jiang Liu, Naijun Zhan, Hengjun Zhao, Liang Zou

Proceedings of the FM 2015: Formal Methods, 2015

Automatic Verification of Stability and Safety for Delay Differential Equations.

Liang Zou, Martin Fränzle, Naijun Zhan, Peter Nazier Mosaad

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Formal Verification of Simulink/Stateflow Diagrams.

Liang Zou, Naijun Zhan, Shuling Wang, Martin Fränzle

Proceedings of the Automated Technology for Verification and Analysis, 2015

Decidability of the Reachability for a Family of Linear Vector Fields.

Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, Naijun Zhan

Proceedings of the Automated Technology for Verification and Analysis, 2015

2014

Discovering non-terminating inputs for multi-path polynomial programs.

Jiang Liu, Ming Xu, Naijun Zhan, Hengjun Zhao

J. Syst. Sci. Complex., 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

Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, 2014

Combining Formal and Informal Methods in the Design of Spacecrafts.

Mengfei Yang, Naijun Zhan

Proceedings of the Engineering Trustworthy Software Systems - First International School, 2014

Formal Verification of a Descent Guidance Control Program of a Lunar Lander.

Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, Yao Chen

Proceedings of the FM 2014: Formal Methods, 2014

Adding Formal Meanings to AADL with Hybrid Annex.

Ehsan Ahmad, Yunwei Dong, Shuling Wang, Naijun Zhan, Liang Zou

Proceedings of the Formal Aspects of Component Software - 11th International Symposium, 2014

2013

Model checking conditional CSL for continuous-time Markov chains.

Yang Gao, Ming Xu, Naijun Zhan, Lijun Zhang

Inf. Process. Lett., 2013

Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation

Deepak Kapur, Naijun Zhan, Hengjun Zhao

CoRR, 2013

Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving.

Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan, Yu Liu

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Formal Modelling, Analysis and Verification of Hybrid Systems.

Naijun Zhan, Shuling Wang, Hengjun Zhao

Proceedings of the Unifying Theories of Programming and Formal Engineering Methods, 2013

An Interface Model of Software Components.

Ruzhen Dong, Naijun Zhan, Liang Zhao

Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013

Bounded model-checking of discrete duration calculus.

Quan Zu, Miaomiao Zhang, Jiaqi Zhu, Naijun Zhan

Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

Super-Dense Computation in Verification of Hybrid CSP Processes.

Dimitar P. Guelev, Shuling Wang, Naijun Zhan, Chaochen Zhou

Proceedings of the Formal Aspects of Component Software - 10th International Symposium, 2013

Towards a Failure Model of Software Components.

Ruzhen Dong, Naijun Zhan

Proceedings of the Formal Aspects of Component Software - 10th International Symposium, 2013

Verifying Simulink diagrams via a Hybrid Hoare Logic Prover.

Liang Zou, Naijun Zhan, Shuling Wang, Martin Fränzle, Shengchao Qin

Proceedings of the International Conference on Embedded Software, 2013

Generating Non-linear Interpolants by Semidefinite Programming.

Liyun Dai, Bican Xia, Naijun Zhan

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants.

Hengjun Zhao, Naijun Zhan, Deepak Kapur

Proceedings of the Theories of Programming and Formal Methods, 2013

CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains.

Yang Gao, Ernst Moritz Hahn, Naijun Zhan, Lijun Zhang

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems.

Jiang Liu, Naijun Zhan, Hengjun Zhao

Math. Comput. Sci., 2012

An Assume/Guarantee Based Compositional Calculus for Hybrid CSP.

Shuling Wang, Naijun Zhan, Dimitar P. Guelev

Proceedings of the Theory and Applications of Models of Computation, 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

Proceedings of the FM 2012: Formal Methods, 2012

Unblockable compositions of software components.

Ruzhen Dong, Johannes Faber, Zhiming Liu, Jirí Srba, Naijun Zhan, Jiaqi Zhu

Proceedings of the 15th ACM SIGSOFT Symposium on Component Based Software Engineering, 2012

2011

Symbolic decision procedure for termination of linear programs.

Bican Xia, Lu Yang, Naijun Zhan, Zhihai Zhang

Formal Aspects Comput., 2011

A Complete Method to Polynomial Differential Invariant Generation for Hybrid Systems

Jiang Liu, Naijun Zhan, Hengjun Zhao

CoRR, 2011

Computing semi-algebraic invariants for polynomial dynamical systems.

Jiang Liu, Naijun Zhan, Hengjun Zhao

Proceedings of the 11th International Conference on Embedded Software, 2011

2010

Connection between logical and algebraic approaches to concurrent systems.

Naijun Zhan

Math. Struct. Comput. Sci., 2010

Rate monotonic scheduling re-analysed.

Qiwen Xu, Naijun Zhan

Inf. Process. Lett., 2010

On hierarchically developing reactive systems.

Naijun Zhan, Mila E. Majster-Cederbaum

Inf. Comput., 2010

Recent advances in program verification through computer algebra.

Lu Yang, Chaochen Zhou, Naijun Zhan, Bican Xia

Frontiers Comput. Sci. China, 2010

Refinement of models of software components.

Zizhen Wang, Hanpin Wang, Naijun Zhan

Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), 2010

A Calculus for Hybrid CSP.

Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou, Liang Zou

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

Refinement and verification in component-based model-driven design.

Zhenbang Chen, Zhiming Liu, Anders P. Ravn, Volker Stolz, Naijun Zhan

Sci. Comput. Program., 2009

Model Checking Linear Duration Invariants of Networks of Automata.

Miaomiao Zhang, Zhiming Liu, Naijun Zhan

Proceedings of the Fundamentals of Software Engineering, 2009

2008

Formalising Scheduling Theories in Duration Calculus.

Qiwen Xu, Naijun Zhan

Nord. J. Comput., 2008

Basic research in computer science and software engineering at SKLCS.

Jian Zhang, Wenhui Zhang, Naijun Zhan, Yi-Dong Shen, Haiming Chen, Yunquan Zhang, Yongji Wang, Enhua Wu, Hongan Wang, Xueyang Zhu

Frontiers Comput. Sci. China, 2008

Component Publications and Compositions.

Naijun Zhan, Eun-Young Kang, Zhiming Liu

Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008

Program Verification by Reduction to Semi-algebraic Systems Solving.

Bican Xia, Lu Yang, Naijun Zhan

Proceedings of the Leveraging Applications of Formal Methods, 2008

2007

Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems.

Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, Chaochen Zhou

Proceedings of the Theoretical Aspects of Computing, 2007

A Model of Component-Based Programming.

Xin Chen, Jifeng He, Zhiming Liu, Naijun Zhan

Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

Modelling with Relational Calculus of Object and Component Systems - rCOS.

Zhenbang Chen, Abdelhakim Hannousse, Dang Van Hung, Istvan Knoll, Xiaoshan Li, Zhiming Liu, Yang Liu, Qu Nan, Joseph C. Okika, Anders P. Ravn, Volker Stolz, Lu Yang, Naijun Zhan

Proceedings of the Common Component Modeling Example: Comparing Software Component Models [result from the Dagstuhl research seminar for CoCoME, 2007

Generating Polynomial Invariants with DISCOVERER and QEPCAD.

Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan

Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2006

Connecting Algebraic and Logical Descriptions of Concurrent Systems.

Naijun Zhan

Proceedings of the Leveraging Applications of Formal Methods, 2006

2005

Program Verification by Using DISCOVERER.

Lu Yang, Naijun Zhan, Bican Xia, Chaochen Zhou

Proceedings of the Verified Software: Theories, 2005

Compositionality of Fixpoint Logic with Chop.

Naijun Zhan, Jinzhao Wu

Proceedings of the Theoretical Aspects of Computing, 2005

Deriving Non-determinism from Conjunction and Disjunction.

Naijun Zhan, Mila E. Majster-Cederbaum

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005

2004

Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity.

Mila E. Majster-Cederbaum, Jinzhao Wu, Houguang Yue, Naijun Zhan

Proceedings of the Formal Methods and Software Engineering, 2004

2003

Compositional Properties of Sequential Processes.

Naijun Zhan

Proceedings of the International Workshop on Software Verification and Validation, 2003

Action Refinement from a Logical Point of View.

Mila E. Majster-Cederbaum, Naijun Zhan, Harald Fecher

Proceedings of the Verification, 2003

Combining Hierarchical Specification with Hierarchical Implementation.

Naijun Zhan

Proceedings of the Advances in Computing Science, 2003

2001

An Intuitive Formal Proof for Deadline Driven Scheduler.

Naijun Zhan

J. Comput. Sci. Technol., 2001

Automatic Synthesis of the DC Specifications of Lip Synchronisation Protocol.

Huadong Ma, Liang Li, Jianzhong Wang, Naijun Zhan

Proceedings of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001), 2001

2000

Another formal proof for Deadline Driven Scheduler.

Naijun Zhan

Proceedings of the 7th International Workshop on Real-Time Computing and Applications Symposium (RTCSA 2000), 2000

Completeness of Higher-Order Duration Calculus.

Naijun Zhan

Proceedings of the Computer Science Logic, 2000

1999

A Formal Proof of the Rate Monotonic Scheduler.

Shuzhen Dong, Qiwen Xu, Naijun Zhan

Proceedings of the 6th International Workshop on Real-Time Computing and Applications Symposium (RTCSA '99), 1999