Publications
See my
page on Google Scholar. See also the DBLP entry for Naijun Zhan.
Most of my papers can be
downloaded below: Please respect the corresponding copyright by the publishers.
For some papers, additional comments and corrections are given in red text in
the pdfs.
Books and book chapters:
[B1]. Chaochen Zhou and Naijun Zhan
(2017): Introduction
to Formal Semantics, Academic Press. (in Chinese)
[B2]. Naijun Zhan, Shuling Wang
and Hengjun Zhao (2016): Formal Verification of Simulink/Stateflow
Diagrams, Springer-Verlag.
[B3]. Mingshuai Chen, Xiao Han, Tao Tang, Shuling Wang, Mengfei
Yang, Naijun Zhan, Hengjun
Zhao, Liang Zou (2017): MARS:
A Toolchain for Modelling, Analysis and Verification of Hybrid Systems. Provably
Correct Systems 2017: 39-58
[B4]. MengfeiYang and Naijun Zhan (2014): Combining Formal and Informal Methods in the
Design of Spacecrafts. In SETSS 2014, Lecture Notes in Computer Science
9506, Springer-Verlag. 2016.
[B5]. Naijun Zhan, Shuling Wang and Hengjun Zhao (2013): Formal Modelling, Analysis and
Verification of Hybrid Systems. In the Theories of Programming,
Lecture
Notes in Computer Science 8050, Springer-Verlag.
Edited volumes and special issues:
[E1]. Marieke Huisman, Corina S. Pasareanu, Naijun Zhan (2023): Formal Methods
Syst. Des. 61(1), special Issue on FM 2021
[E2]. Marieke Huisman, Corina S. Pasareanu, Naijun Zhan (2023): Formal Aspects Comput. 35(2), special Issue on FM 2021
[E3]. Marieke Huisman, Corina S. Pasareanu, Naijun Zhan (2021): Formal Methods
- 24th International Symposium, FM 2021, Virtual Event, November
20-26, 2021, Proceedings. Lecture Notes in Computer Science 13047, Springer 2021, ISBN 978-3-030-90869-0. (Editor)
[E4]. Partha S. Roop, Naijun Zhan, Sicun Gao, Pierluigi Nuzzo
(2019): Proceedings
of the 17th ACM-IEEE International Conference on Formal Methods and Models for
System Design, MEMOCODE 2019, La Jolla, CA, USA, October 9-11,
2019. ACM 2019, ISBN 978-1-4503-6997-8. (Editor)
[E5]. Cliff B. Jones, Ji Wang, Naijun Zhan (2017): Symposium on
Real-Time and Hybrid Systems - Essays Dedicated to Professor Chaochen Zhou on the Occasion of His 80th Birthday. Lecture Notes in Computer Science 11180, Springer2018, ISBN 978-3-030-01460-5.
(Editor)
[E6]. Martin Fränzle, Deepak Kapur, Naijun Zhan (2016): Dependable Software
Engineering: Theories, Tools, and Applications - Second International Symposium, SETTA
2016, Beijing, China, November 9-11, 2016, Proceedings. Lecture Notes in
Computer Science 9984, ISBN 978-3-319-47676-6. (Editor)
[E7]. Martin Fränzle, Deepak Kapur, Heike Wehrheim, Naijun Zhan (2019): Formal
Aspects Comput. 31(1), special issue on SETTA 2016.
[E8]. Arvind Easwaran, Qi Zhu, Naijun Zhan (2020): Journal
of Systems Architecture, special Issue on ICESS 2019
[E9]. Naijun Zhan, Xuandong Li and Ji Wang (2016): Journal
of Software 27(3), special issue on formal methods and its
application. (in Chinese)
Journal papers:
[J1].
Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi and Zhihong Yang (2024): Synthesizing Invariants for Polynomial Programs by
Semidefinite Programming. ACM
Transactions on Programming Languages and Systems, in press.
[J2].
Naijun Zhan, Han Su, Mengfei
Yang and Bin Gu (2024): Reset Controller Synthesis: A Correct-by-Construction Way to the
Design of CPS. Research
Direction: Cyber-Physical Systems, 2(e7):1-7.
[J3]. Chenhao Wu, Rruoxiang
Li, Naijun Zhan, Nan Guan (2024): Modelling
and Analysis of the LatestTime Message Synchronization Policy in ROS. IEEE
Transactions on Computer-Aided Design of Integrated Circuits and Systems, 43(11): 3576-3587. (Special issue
of EMSOFT 2024)
[J4]. Bai Xue,
Naijun Zhan and Martin Fränzle
(2023): Reach-Avoid Analysis for Stochastic Differential
Equations. IEEE
Transactions on Automatic Control, 69(3): 1882-1889.
[J5]. Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia and Naijun Zhan (2024): Decision Procedure for String Constraints with String-Integer Conversion and Flat Regular Constraints. Acta Informatica, 61(1): 23-52.
[J6]. Bai Xue,
Naijun Zhan, Martin Fränzle, Ji Wang, Wanwei Liu (2024): Reach-avoid
Verification Based on Convex Optimization. IEEE Transactions
on Automatic Control, 69(1): 598-605.
[J7].
Shenghua Feng, Mingshuai
Chen, Han Su, Benjamin Lucien
Kaminski, Joost-Pieter Katoen, Naijun Zhan (2023). Lower Bounds for Possibly Divergent
Probabilistic Programs. In Proc. ACM Program. Lang., (OOPSLA), 7: 696-726.
[J8]. Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen (2022): Encoding inductive invariants as barrier certificates synthesis via difference-of-convex programming. Information and Computation 289:104965 (Extended version of CAV 2021 paper)
[J9].
Xiong Xu, Bohua Zhan, Shuling
Wang, Jean-Pierre Talpin and Naijun
Zhan (2022): A denotational semantics of Simulink
with higher-order UTP. Journal
of Logical and Algebraic Methods in Programming, 130: 100809.
[J10].
Tengshun Yang, Shuling Wang, Bohua
Zhan, Naijun Zhan, Jinghui Li, Shuangqing
Xiang, Zhan Xiang,
Bifei Mao (2022): Formal
Analysis of 5G AKMA. Journal
of System Architecture, 126: 102478.
[J11].
Xiong Xu, Bohua Zhan, Shuling
Wang, Jean-Pierre Talpin and Naijun
Zhan (2022): Semantics
foundation for cyber-physical systems using higher-order UTP. ACM
Transactions on Software Engineering and Methodology, 32(1), Article No. 9:1-48.
[J12].
Xiong Xu, Bohua Zhan, Shuling
Wang, Xiangyu Jin,
Jean-Pierre Talpin and Naijun
Zhan (2021): Unified graphical co-modeling,
analysis and verification of cyber-physical systems by combining AADL and
Simulink/Stateflow. Theoretical
Computer Science, 903:1-25.
[J13].
Jie An, Bohua Zhan, Naijun
Zhan and Miaomiao Zhang (2021): Learning Nondeterministic Real-Time
Automata, ACM Transaction on Embedded Computing
Systems, Article 7:1-25, special issue of EMSOFT 2021, 20(5s) 99:1-99:26.
[J14]. Wenyou Liu, Yunjun
Bai, Li Jiao, Bai Xue and Naijun
Zhan (2023): Safety Guarantee for Time-Delay
Systems with Disturbances by Control Barrier Functionals, Science
China Information Science, 66: 132102.
[J15].
Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan and Miaomiao Zhang (2021): Inferring Nonlinear Switched
Dynamical Systems. Formal
Aspects of Computing, 33(3): 385-406.
[J16].
Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue and Naijun Zhan (2021): Switching
Controller Synthesis for Time-delayed Hybrid Systems. Science
China Mathematica, 51(1):97-114. (in Chinese)
[J17].
Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang and Zhikun She (2021): Synthesizing robust domains of attraction
for state-constrained perturbed polynomial systems. SIAM
J. on Control and Optimization, 59(2): 1083-1108.
[J18].
Bai Xue and Naijun Zhan (2022): Robust Invariant Sets Computation
for Discrete-Time Perturbed Nonlinear Systems. IEEE Transactions
on Automatic Control, 67(2):1053-1060.
[J19].
Bai Xue, Martin
Fränzle, Naijun Zhan, Sergiy Bogomolov and Bican Xia (2020): Safety Verification for Random Ordinary
Differential Equations. IEEE Transactions on Computer-Aided
Design of Integrated Circuits and Systems,39(11):4090-4101. (Special issue
of EMSOFT 2020)
[J20].
Mingshuai Chen,
Martin Fraenzle, Yangjia
Li, Peter N. Mosaad and Naijun
Zhan (2020): Indecision and delays are the
parents of failure – Taming them algorithmically by synthesizing
delay-resilient control.
Acta Informatica, 58(5): 497-528.
[J21].
Bai Xue, Qiuye Wang, Shenghua Feng and Naijun Zhan
(2020): Over- and Under-Approximating Reach
Sets for Perturbed Delay Differential Equations.
IEEE Transactions on Automatic Control, 66(1): 283-290.
[J22].
Jie An, Lingtai Wang, Bohua
Zhan, Naijun Zhan and Miaomiao
Zhang (2020): Learning real-time automata. Science
China Information Science, 64:192103:1–192103:17.
[J23].
Jian Wang, Jie An, Mingshuai Cheng, Naijun
Zhan, Lulin Wang, Miaomiao
Zhang, and Ting Gan (2020): From model to implementation: A
network algorithm programming language. Science China Information Science,
63(7):172102:1–172102:17.
[J24].
Gaogao Yan, Li Jiao, Shuling Wang, Lingtai Wang and Naijun Zhan
(2020): Automatically
generating SystemC code from HCSP formal mdoels. ACM Transactions on Software
Engineering and Methodology, 29(1), Article 4:1-39. (Extended version of FM 2016 paper)
[J25].
Bai Xue, Martin Fraenzle and Naijun Zhan (2020):
Inner approximating reachable sets
for polynomial systems with time-varying uncertainties.
IEEE Transactions on Automatic Control, 65(4):1468-1483.
[J26].
LingtaiWang, Naijun Zhan and Jie
An (2018)：The
opacity of real-time automata. IEEE
Transactions on Computer-Aided Design of Integrated Circuits and Systems, 37(11): 2845-2856. (Special issue of EMSOFT 2018)
[J27].
Ting Gan,
Mingshuai Chen, Yangjia Li, Bican
Xia and Naijun Zhan (2018): Reachability
analysis for solvable dynamical systems.
IEEE Transactions on Automatic Control, 63(7): 2003-2018.
[J28].
Qiuye Wang, Yangjia Li, Bican
Xia and Naijun Zhan (2017): Generating
semi-algebraic invariants for non-autonomous hybrid systems. Journal
of System Science and Complexity, 30(1):234-253.
[J29].
Shuling Wang, Naijun Zhan and Lijun Zhang (2017): A
compositional modelling and verification framework for stochastic hybrid
systems.
Formal Aspects of Computing, 29(4):751-775. (extended
version of SETTA 2015 paper)
[J30].
Shuling Wang, Flemming Nielson, Hanne Riis Nielson and
Naijun Zhan (2017): Modelling
and Verifying Communication Failure of Hybrid Systems in HCSP.
Computer Journal, 60(8):1111-1130.
[J31].
Liyun Dai, Ting Gan, Bican Xia and Naijun Zhan (2017): Barrier
certificate revisited. Journal
of Symbolic Computation, 80:62-86.
[J32].
Ehsan Ahmad, Yunwei Dong, Brian Larsen, Jidong
Lv, Tao Tang and Naijun
Zhan (2015): Behavior modeling and verification
of movement authority scenario of Chinese Train Control System using AADL. Science
China Information Sciences, 58(11):1-20.
[J33].
Danqing Guo, Jidong Lv, Shuling Wang, Tao Tang, Naijun
Zhan, Datian Zhou and Liang Zou (2015): Formal
anlysis and verification of Chinese Train Control System. Science
China Information Sciences, 45(3):417-438 (in Chinese).
[J34].
Jiang Liu, Ming
Xu, Naijun Zhan and Hengjun
Zhao (2014): Discovering non-terminating inputs
for polynomial programs. Journal of
System Science and Complexity, 27(6):1286-1304.
[J35]. Yang Gao, Ming Xu, Naijun
Zhan and Lijun Zhang (2013): Model-checking Conditional CSL for
Continuous-time Markov Chains. Information
Processing Letters, 113(1-2):44-50.
[J36]. Jiang Liu, Naijun Zhan, and Hengjun Zhao (2012): Automatically
discovering relaxed Lyapunov functions for polynomial dynamical systems. Mathematics
in Computer Science, 6:395-408, 2012.
[J37]. Bican Xia, Lu Yang, Naijun
Zhan and Zhihai Zhang (2011): Symbolic
decision procedure for termination. Formal
Aspects of Computing, 23(2):171-190, 2011. DOI: 10.1007/s00165-009-0144-5.
[J38]. Qiwen Xu and Naijun
Zhan (2010): Rate Monotonic Scheduling Re-analyzed. Information
Processing Letters, 110(6): 226-231. DOI: 10.1016/j.ipl.2009.12.010
[J39]. Naijun Zhan (2010): Connection between algebraical and logical
approaches to concurrent systems. Mathematical
Structures in Computer Science, 20(5):915-950.
[J40]. Yang Lu, Chaochen Zhou, Naijun Zhan and Bican Xia (2010):
Recent advances in program verification through
computer algebra. Frontiers of
Computer Science in China, 4(1):1-16.
[J41]. Naijun Zhan and Mila Majster-Cederbaum
(2010): On
hierarchically developing reactive systems. Information
and Computation, 208(9):997-1019.
[J42]. Zhenbang Chen, Zhiming
Liu, Volker Stolz, Anders P. Ravn, and Naijun Zhan (2009): Refinement
and verification in component based and model driven design. Science
of Computer Programming, 74(4):168-196.
[J43]. Xu Qiwen and Naijun Zhan (2008): Formalizing
scheduling theorems using duration calculus. Nordic
Journal of Computing, 14:173- 201.
[J44]. Jian Zhang, Wenhui Zhang, Naijun Zhan, Yidong Shen, Haiming Chen, Yunquan Zhang, Yongji Wang, Enhua Wu, Hongan Wang, and Xueyang Zhu
(2008): Basic research in computer
science and software engineering at SKLCS. Frontiers of Computer Science in China, 2(1): 1-11.
[J45]. Naijun Zhan (2004): Compositional
properties of sequential processes. Electronic
Notes in Theoretical Computer Science, 118:111-128.
[J46]. Naijun Zhan (2001): A
higher-order duration calculus and its completeness. Science
China, Vol 30(5).
[J47]. Naijun Zhan (2001): An intuitive proof for DDS. Journal
of Computer Science and Technology, 16(2):146-158.
Peer-reviewed Conferences and Workshops:
[C1]. Xiong Xu, Jean-Pierre Talpin,
Shuling Wang, Bohua Zhan, Xinxin Liu, Naijun Zhan
(2025): HpC: A Calculus for Hybrid and Mobile Systems.
Accepted by OOPSLA 2025.
[C2]. Xiong Xu, Shuling
Wang, Zekun Ji, Qiang Gao, Xiangyu Jin, Bohua
Zhan and Naijun Zhan (2024): Case Study: Modeling, Simulation,
Verification, and Code Generation of an Automatic Cruise Control System. In the Proc. of the Festschrift of Cliff
Jones’ 80th birthday, Lecture Notes in Computer Science 14781, pp.226-246.
[C3]. Shenghua Feng, Tengshun
Yang, Mingshuai Chen, and Naijun Zhan (2024): A
Unified Framework for Quantitative Analysis of Probabilistic Programs.
In the Proc. of Colloquium on Principles of Verification: Cycling the
Probabilistic Landscape, Festschrift of Prof. Joost-Pieter Katoen’s
60th birthday, Lecture Notes in Computer Science 15260, pp.230-254.
[C4]. Shangshang Xiao, Mengxia
Sun, Wei Zhang, Naijun Zhan, Lei Ju (2024): Cache
Behavior Analysis with SP-Relative Addressing for WCET Estimation. In the Proc. of SETTA
2024, Lecture Notes in Computer Science 15469, pp.217-235.
[C5]. Yihao Yin, Hao Wu, Shuling
Wang, Xiong Xu, Fanjiang
Xu, and Naijun Zhan (2024): The Design of Intelligent Temperature
Control System of Smart House with MARS. In the Proc. of SETTA 2024, Lecture Notes in Computer Science 15469, pp.217-235.
[C6]. Chenhao
Wu, Rruoxiang Li, Naijun
Zhan, Nan Guan (2024):Modelling and Analysis of the
LatestTime Message Synchronization Policy in ROS. Accepted
by EMSOFT 2024, to
appear IEEE Transactions on
Computer-Aided Design of Integrated Circuits and Systems.
[C7]. Han Su, Shenghua
Feng, Sinong Zhan and Naijun Zhan (2024): Switching
Controller Synthesis for Hybrids Systems Against STL Formulas. In Proc. of FM 2024, Lecture Notes in
Computer Science 14934, pp. 229-247.
[C8]. Hao Wu, Shenghua Feng, Ting
Gan, Jie Wang, Bican Xia
and Naijun Zhan (2024): On
Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains. In Proc. of FM 2024, Lecture Notes in
Computer Science 14934, pp.248-266.
[C9]. Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan and Ting Gan (2024): Nonlinear
Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic
Sets. In Proc. of FM 2024, Lecture Notes in
Computer Science 14933, pp.92-110.
[C10]. Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan and
Ichiro Hasuo (2024): The
Opacity of Timed Automata. In Proc. of FM 2024, Lecture Notes in
Computer Science 14933, pp.620-637.
[C11]. Chenhao Wu, Ruoxiang Li,
Naijun Zhan and Nan Guan (2024): Improving
the Reaction Latency Analysis of Message Synchronization in ROS. In Proc. of RTCSA 2024, pp. 43-48.
[C12]. Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, and Naijun Zhan
(2024): Formally
Verified C Code Generation from Hybrid Communicating Sequential Processes
(a
full version). In Proc. of ICCPS 2024, pp.123-134.
[C13]. Shicheng Yi, Shuling
Wang, Bohua Zhan and Naijun
Zhan (2022): An Executable Semantics for Stateflow in
Isabelle/HOL. In Proc. of ICFEM 2022, Lecture
Notes in Computer Science 13478, pp.421-438.
[C14]. Xiaochen Tang, Wei Shen, Miaomiao
Zhang, Jie An, Bohua Zhan
and Naijun Zhan (2022): Learning
Deterministic One-Clock Timed Automata via Mutation Testing. In Proc. of ATVA 2022. Lecture Notes in Computer Science 13505,
pp.233-248.
[C15]. Bai Xue, Qiuye
Wang, Naijun Zhan, Martin Frnzle,
Shenghua Feng (2022): Differential Games Based on Invariant Sets
Generation. In Proc. of ACC 2022, pp. 1285-1292
[C16]. Tengshun Yang, Shuling
Wang, Bohua Zhan, Naijun
Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang and Bifei Mao (2021): Formal Analysis of 5G AKMA. In Proc. of SETTA 2021, Lecture Notes in Computer Science 13071, pp.102-121.
[C17]. Bai Xue, Yunjun
Bai, Naijun Zhan, Wenyou
Liu and Li Jiao (2021): Reach-Avoid
Analysis for Delay Differential Equations. CDC
2021, pp.1301-1307.
[C18]. Jie An, Bohua Zhan, Naijun Zhan and Miaomiao Zhang
(2021): Learning Nondeterministic Real-Time
Automata. Accepted by EMSOFT 2021.
[C19]. Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan and Joost-Pieter
Katoen (2021): Synthesizing Invariant Barrier Certificates
via Difference-of-Convex Programming, a submitted version and a full version. In Proc. of CAV
2021, Lecture Notes in Computer Science 12759, pp.443-466.
[C20]. Bohua Zhan, Bin Gu, Xiong
Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao Chen, Mengfei
Yang and Naijun Zhan (2021): Modeling
and Verification of Descent Guidance Control of Mars Lander. In Proc. of RTAS 2021 (a brief industry paper),
pp.457-460.
[C21]. Bai Xue, Renjue
Li, Naijun Zhan, Martin Fränzle (2021): Reach-avoid Analysis for Stochastic
Discrete-time Systems. In Proc. of ACC 2021, pp.4879-4885.
[C22]. Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue and Naijun Zhan (2021): Switching Controller Synthesis for
Time-delayed Hybrid Systems under Perturbation. In Proc. of HSCC
2021, pp. 3:1-3:11.
[C23]. Bai Xue and Naijun Zhan (2020): Probably Approximately Correct Interpolants
Generation. In Proc. of SETTA 2020, Lecture Notes in Computer Science, 12153, pp.
143-159.
[C24]. Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue and Naijun Zhan (2020): PAC
learning of deterministic one-clock timed automata. In Proc. of
ICFEM 2020, Lecture Notes in Computer Science 12531,
pp.129-146.
[C25]. Bai Xue, Naijun Zhan
and Martin Fränzle (2020): Inner-approximating
reach-avoid sets for discrete-time polynomial systems. In Proc. of CDC 2020, pp. 867-873.
[C26]. Bai Xue, Martin Fränzle, Naijun Zhan, Sergiy Bogomolov and Bican Xia (2020): Safety
Verification for Random Ordinary Differential Equations. In Proc. of EMSOFT
2020, proceedings was
appeared as special issue of IEEE TCAD.
[C27]. Shenghua Feng, Mingshuai Chen, Sriram Sankaranarayanan, Bai Xue and Naijun Zhan (2020):Unbounded-time
Safety Verification of Stochastic Differential Dynamics. In Proc. of CAV
2020, Lecture
Notes in Computer Science 12224, pp.327-348.
[C28]. Ting Gan, Bican
Xia, Bai Xue, Naijun Zhan
and Liyun Dai (2020): Non-linear
Interpolant Generation. In Proc. of CAV
2020, Lecture
Notes in Computer Science 12225, pp.415-438.
[C29]. Bai Xue, Naijun Zhan and Yangjia Li
(2020):
Robust Regions of Attraction Generation for State-Constrained Perturbed
Discrete-Time Polynomial Systems. In Proc. of IFAC
2020.
[C30]. Bai Xue, Naijun Zhan and Yangjia Li
(2020): A Characterization
of Robust Regions of Attraction for Discrete-Time Systems Based on Bellman
Equations. In Proc. of IFAC
2020.
[C31]. Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan and Miaomiao Zhan (2020): Learning
one-clock timed automata. In Proc. of TACAS
2020, Lecture
Notes in Computer Science 12078,
pp.444-462.
[C32]. Naijun Zhan (2019): Taming
delays in cyber-physical systems. In Proc. of ICFEM
2019, Lecture
Notes in Computer Science 11852, pp.
xv-xvii. (the
extend abstract of an invited talk)
[C33]. Bai Xue, Martin Fraenzle, Hengjun Zhao, Naijun Zhan and Arvind Easwaran (2019): Probably
Approximate Safety Verification of Hybrid Dynamical Systems. In Proc. of ICFEM
2019, Lecture
Notes in Computer Science 11852, pp.
236-252.
[C34]. Stefan Mitsch, Andrew
Sogokon, Yong
Kiam Tan, Xiangyu Jin, Bohua
Zhan, Shuling Wang, Naijun Zhan (2019):ARCH-COMP19
Category Report: Hybrid Systems Theorem Proving.
ARCH@ CPSIoTWeek 2019: 141-161
[C35]. Haolan Zhan, Qianqian
Lin, Shuling Wang, Jean-Pierre Talpin,
Xiong Xu and Naijun Zhan
(2019): Unified
Graphical Co-Modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow. In Proc. of UTP
2019, Lecture
Notes in Computer Science 11885, pp.
109-129.
[C36]. Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle
and Bai Xue (2019): Taming
Delays in Dynamical Systems: Unbounded Verification of Delay Differential
Equations. In Proc. of CAV
2019, Lecture
Notes in Computer Science 11561,
pp.650-669.
[C37]. Junyi Liu, Bohua
Zhan, Shuling Wang, Shenggang
Ying, Tao Liu, Yangjia Li, Mingsheng
Ying and Naijun Zhan (2019): Formal
verification of quantum algorithms using quantum Hoare logic. In Proc. of CAV
2019, Lecture
Notes in Computer Science 11562,
pp.187-207.
[C38]. Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur and Naijun Zhan (2019): NIL:
Learning Nonlinear Interpolants. In Proc. of CADE
2019, , Lecture Notes in Computer Science 11716,
pp.178-196.
[C39]. Bai Xue, Qiuye Wang, Naijun Zhan and Martin Fraenzle (2019): Robust Invariant Sets Generation for State-Constrained Perturbed Polynomial Systems. In Proc. of HSCC 2019, pp. 128-137.
[C40]. Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun
Zhan (2018): ARCH-COMP18 Category Report: Hybrid Systems
Theorem Proving. ARCH@ADHS 2018: 110-127
[C41]. Lingtai Wang, Naijun
Zhan and Jie An (2018): The
opacity of real-time automata. In Proc. of EMSOFT 2018. (Also to appear in the
special issue of IEEE TCAD for EMSOFT 2018)
[C42]. Mingshuai Chen, Martin Fraenzle,
Yangjia Li, Peter N. Mosaad
and Naijun Zhan (2018): What’s
to come is still unsure: Synthesizing synthesizers resilient to delayed
reaction. In ATVA
2018, Lecture
Notes in Computer Science 11138, pp.56-74. (distinguished paper awards)
[C43]. Bai Xue, Naijun
Zhan, Yangjia Li and Qiuye
Wang (2018): Robust Non-termination Analysis of
Numerical Software. In Proc. of SETTA 2018, Lecture Notes in Computer Science 10998, pp. 69-88. (best paper awards)
[C44]. Lingtai Wang and Naijun
Zhan (2018): Decidability
of the initial-state opacity of real-time automata. In Proc. of Symposium on Real-time and
Hybrid Systems in Honor of Prof. Chaochen
Zhou’s 80th Birthday, Lecture Notes in Computer Science 11180, pp. 40-60.
[C45]. Yijun Feng, Joost-Pieter Katoen,
Haokun Li, Bican Xia and Naijun Zhan (2018): Monitoring
CTMCs by multi-clock timed automata. In Proc. of CAV 2018, Lecture Notes in Computer Science 10981, pp.
507-526.
[C46]. Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang and Wang Yi (2018): Model-checking continuous-time bounded
extended linear duration invariants. In
Proc. of HSCC 2018, pp.81-90.
[C47]. Bai Xue, Martin Fraenzle and Naijun Zhan (2018): Under-Approximating
Reach Sets for Polynomial Continuous Systems. In Proc. of HSCC 2018, pp.51-60.
[C48]. Dimitar P. Guelev, Shuling Wang, Naijun Zhan
(2017): Compositional Hoare-Style Reasoning About
Hybrid CSP in the Duration Calculus. In Proc. of SETTA2017, Lecture Notes in Computer Science 10606, pp.110-127.
[C49]. Gaogao Yan, Li Jiao, Shuling
Wang and Naijun Zhan (2017): Generating
SystemC code from delay HCSP. In Proc. of APLAS 2017, Lecture Notes in Computer Science 10695, pp.21-41.
[C50]. Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan and Bican Xia (2017):
Finding polynomial loop invariants for
probabilistic programs, in Proc. of ATVA 2017, Lecture Notes in Computer Science 10484, pp.
400-416.
[C51]. Bai Xue, Peter Nazier Mosaad, Martin Fraenzle, Mingshuai Chen, Yangjia
Li and Naijun Zhan (2017): Safe
over- and under-approximation of reachable sets for delay differential
equations, in Proc.
of FORMATS 2017, Lecture Notes in
Computer Science 10419, pp.281-299. (It contains some mistakes,
a corrected version is downloadable here)
[C52]. Gaogao Yan and Li Jiao and Yangjia
Li and Shuling Wang and Naijun
Zhan (2016): Approximate bisimulation and discretization
of Hybrid CSP, in Proc. of FM 2016, Lecture Notes in Computer Science 9995, pp.702-720.
[C53]. Mingshuai Chen and Martin Fraenzle
and Yangjia Li and Peter N. Mosaad
and Naijun Zhan (2016): Validated
simulation-based verification of delayed differential dynamics, in Proc. of FM 2016, Lecture
Notes in Computer Science 9995, pp.137-154.
[C54]. Mingshuai Chen, Anders P. Ravn,
Shuling Wang, Mengfei Yang,
and Naijun Zhan (2016): A
two-way path between formal and informal design of embedded systems, in Proc. of UTP 2016, Lecture Notes in Computer Science 10134, pp.65-92.
[C55]. Ting Gan, Mingshuai Chen, Yangjia
Li, Bican Xia and Naijun
Zhan (2016): Computing reachable sets of linear vector
fields revisited, in Proc. of ECC 2016, pp.419-426.
[C56]. Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur and Mingshuai Chen (2016): Interpolant
synthesis for quadratic polynomial inequalities and combination with EUF, in Proc. of IJCAR 2016, Lecture Notes in Computer Science 9706,
pp.195-212.
[C57]. Yu Peng, Shuling Wang, Naijun
Zhan, Lijun Zhang (2015): Extending
Hybrid CSP with Probability and Stochasticity, in Proc. SETTA 2015, Lecture Notes in Computer Science 9409, pp.87-102.
[C58]. S. Wang, N. Zhan and L. Zou (2015): An
improved HHL prover: An interactive theorem prover for hybrid systems, in Proc. of ICFEM 2015, Lecture Notes in
Computer Science 9407, pp.282-399.
[C59]. Ting Gan, Mingshuai Chen, Liyun
Dai, Bican Xia and Naijun
Zhan (2015): Decidability of the reachability for a family of
linear vector fields, in Proc. of ATVA
2015, Lecture Notes in Computer
Science 9364, pp.482-499.
[C60]. Liang Zou, Naijun Zhan, Shuling Wang and Martin Fraenzle
(2015): Formal verification of Simulink/Stateflow
diagrams, in Proc. of ATVA
2015, Lecture Notes in Computer Science 9364, pp.482-499.
[C61]. Liang Zou, Martin Fraenzle, Naijun Zhan and Peter Nazier Mosaad (2015): Automatic
stability and safety verification for delay differential equations, in Proc. of CAV 2015, Lecture Notes in Computer Science 9364, pp.338-355.
[C62]. Jiang Liu, Naijun Zhan, Hengjun Zhao and Liang Zou (2015): Abstraction
of elementary hybrid systems by variable transformation, in Proc. of FM 2015, Lecture Notes in Computer Science 9109, pp.360-377.
[C63]. Naijun Zhan and Liang Zou (2014): Formal verification of Simulink/Stateflow diagrams, in Proc. of ESWEEK 2014 (abstract only).
[C64]. Ehsan Ahmad, Brian Larson, Stephen Barrett, Naijun Zhan and Yunwei Dong
(2014): An AADL Extension for Continuous Behavior
and Cyber-Physical Interaction Modeling, in Proc. of HILT 2014, pp.29-38.
[C65]. Ehsan Ahmad, Yunwei Dong, Shuling Wang, Naijun Zhan and
Liang Zou (2014): Adding Formal Meanings to AADL Models with
Hybrid Annex, in Proc. of FACS 2014, Lecture Notes in Computer Science 8997, pp.228-247.
[C66]. Hengjun Zhao, Mengfei Yang,
Naijun Zhan, Bin Gu, Liang Zou and Yao Chen (2014): Formal
verification of a descent guidance control program of a lunar lander, in Proc. of FM 2014, Lecture Notes in
Computer Science 8442, pp.733-748.
[C67]. Ruzhen Dong and Naijun
Zhan (2013): Towards a failure model of software
components, in Proc. of FACS 2013, Lecture Notes in
Computer Science 8348, pp.119-136.
[C68]. Dimitar P. Guelev, Shuling Wang, Naijun
Zhan and Chaochen Zhou (2013): Super-dense
computation in verification of HCSP processes, in Proc. of FACS 2013, Lecture Notes in
Computer Science 8348, pp.13-22.
[C69]. Liang Zou, Naijun Zhan, Shuling Wang, Martin Fraenzle and
Shengchao Qin (2013): Verifying
Simulink diagrams via a Hybrid Hoare Logic prover, in Proc. of EMSOFT 2013, pp.1-10.
[C70]. Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan and Yu Lei (2013): Verifying
Chinese train control system under a combined scenario by theorem proving, in Proc. of VSTTE 2013, Lecture Notes in
Computer Science 8164, pp.262-280.
[C71]. Yang Gao, Ernst Moritz Hahn, Naijun
Zhan and Lijun Zhang (2013): A
CSL model checker for continuous-time markov chains, in Proc. of ATVA 2013, Lecture Notes in
Computer Science 8172, pp.464-468.
[C72]. Ruzhen Dong, Naijun
Zhan and Liang Zhao (2013): An
interface model of software components, in Proc. of ICTAC 2013, Lecture Notes in
Computer Science 8049, pp.159-176.
[C73]. Hengjun Zhao, Naijun
Zhan and Deepak Kapur (2013): Synthesizing
switching controllers for hybrid systems by generating invariants, in Proc. of the Jifeng Festschrift, Lecture Notes in Computer Science 8051,
pp.354-373.
[C74]. Liyun Dai, Bican Xia
and Naijun Zhan (2013): Generating
non-linear interpolants by semi-definite programming, in Proc. of CAV 2013, Lecture Notes in
Computer Science 8044, pp.364-380.
[C75]. Quan Zu, Miaomiao
Zhang, Jiaqi Zhu and Naijun
Zhan (2013): Bounded model-checking of discrete Duration
Calculus, in
Proc. of HSCC 2013, pp.213-222.
[C76]. Hengjun Zhao, Naijun
Zhan, Deepak Kapur, and Kim G. Larsen (2012): A
“hybrid” approach for synthesizing optimal controllers of hybrid
systems: A Case study of the oil pump industrial example, in Proc. of FM 2012, Lecture Notes in
Computer Science 7436, pp.471-485, 2012.
[C77]. Shuling Wang, Naijun
Zhan and Dimitar Guelev
(2012): An assume/guarantee based compositional
calculus for Hybrid CSP. A keynotes of TAMC 2012, Lecture Notes in Computer Science 7287, pp.72-83.
[C78]. Ruzhen Dong, Johannes Farber, Zhiming
Liu, Jiri Srba, Naijun
Zhan, and Jiaqi Zhu (2012): Unblockable
compositions of software components, in Proc. of CBSE 2012, ACM SIGSOFT.
[C79]. Jiang Liu, Naijun Zhan and Hengjun Zhao (2011):Computing
semi-algebraic invariants for polynomial dynamical systems, in Proc. of EMSOFT 2011, pp.97-106, ACM Press.
[C80]. Jiang Liu, Naijun Zhan and Hengjun Zhao (2011): Automatically
discovering relaxed Lyapunov functions for polynomial dynamical systems, in
Proc. of MACIS 2011, pp.162-177.
[C81]. ZizhenWang, HanpinWang and Naijun Zhan (2010): Refinement
theories of software components. ACM
SIGAPP SAC 2010, pp.2311-2318.
[C82]. Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou and
Liang Zou (2010): A
calculus for HCSP. A keynotes of APLAS 2010, Lecture Notes in Computer Science 6461, pp. 1-15.
[C83]. Miaomiao Zhang, Zhiming
Liu and Naijun Zhan (2009): Model
checking linear duration invariants of networks of automata. In Proc. FSEN 2009, Lecture Notes in
Computer Science 5961 pp.244-259.
[C84]. Naijun Zhan, Eoun-Yound
Kang and Zhiming Liu (2008): Refinement
and composition of components in rCOS. In Proc. of UTP 2008, Lecture Notes in
Computer Science 5713, pp.238-257.
[C85]. Bican Xia, Lu Yang and Naijun
Zhan (2008): Program verification by reduction to
semi-algebraic systems solving, in Proc. of ISoLA 2008, CCIS 17, Springer-Verlag, pp277-291.
[C86]. Zhenbang Chen, Abdel Hakim 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 (2007): Modelling
with Relational Calculus of Object and Component Systems - rCOS. In Proc. of CoCoME, Lecture Notes in Computer Science 5153, pp. 116-145.
[C87]. Xin Chen, Jifeng He, Zhiming Liu and Naijun Zhan
(2007): A model of compoent-based programming. In Proc. Of FSEN 2007, Lecture Notes in
Computer Science 4774.
[C88]. Yinghua Chen, Bican Xia,
Lu Yang, and Naijun Zhan (2007): Reducing
polynomial invariant generation to semi-algebraic systems solving. In Proc. of Festschrift Symposium in honour of Dines Bjorner and Zhou Chaochen, Lecture Notes in Computer Science 4700.
[C89]. Yinghua Chen, Bican Xia,
Lu Yang, Naijun Zhan and Chaochen
Zhou (2007): Discovering
non-linear ranking functions by solving semi-algebraic systems. In Proc. of ICTAC 2007, Lecture Notes in
Computer Science 4711.
[C90]. Naijun Zhan (2006): Connecting algebraical and logical
descriptions of concurrent systems. In the Proc. of ISoLA 2006, IEEE Computer Society Press.
[C91]. Naijun Zhan, Dang Van Hung, Zhiming
Liu and Xiaoshan Li (2006): Towards a theory of component-based real-time systems. In the proc.
AWCVS 2006, preliminary proceedings
as number 348 in UNU-IIST Reports, P.O.Box
3058, Macau.
[C92]. Naijun Zhan and Jinzhao
Wu (2005): Compositionality of fixpoint logic with chop. In the Proc. of ICTAC 2005, Lecture Notes
in Computer Science 3722, pp.136-150.
[C93]. Naijun Zhan and Mila Majster-Cederbaum
(2005): Deriving nondeterminism from conjunction
and disjunction. In the proc. of 25th IFIPWG 6.1
International Conference on Formal Techniques on Networked and Distributed
Systems (FORTE 2005), Lecture Notes in Computer Science 3731,
pp. 351-365.
[C94]. Lu Yang, Naijun Zhan, Bican Xia and Chaochen Zhou
(2005): Program verification by using DISCOVERER. In the Proc. of VSTTE 2005, Lecture Notes in
Computer Science 4171,
pp.528-538.
[C95]. Mila Majster-Cederbaum, Jinzhao Wu, Houguang Yue, Naijun Zhan (2004): Refinement
of actions for real-time concurrent systems with causal ambiguity. In the Proc. of ICFEM 2004, Lecture Notes in
Computer Science 3308, pp. 449-463.
[C96]. Naijun Zhan (2003): Combining
hierarchical specification with hierarchical implementation. In the Proc. of ASIAN 2003, Lecture Notes in
Computer Science 2896, pp. 110-124.
[C97]. M. Majster-Cederbaum, Naijun Zhan and Harald Fecher
(2003): Action refinement from a logical point of
view. In the Proc. of VMCAI 2003, Lecture Notes in
Computer Science 2575, pp.253-267.
[C98]. Huandong Ma, Liang Li, Jianzhong
Wang, Naijun Zhan (2001): Automatic synthesis of the
DC specifications of Lip synchronization protocol. In the proc. of APSEC 2001, IEEE Computer Society
Press.
[C99]. Naijun Zhan (2000): Completeness
of higher-order duration calculus. In the proc. of CSL 2000, Lecture Notes in Computer Science 1863.
[C100]. Naijun Zhan: Another
formal proof for deadline driven scheduler. In the Proc. of RTCSA'00, IEEE Computer Society Press.
[C101]. Chaochen Zhou, Dimitar P.
Guelev and Naijun Zhan
(1999): A higher-order duration calculus. In the Proc. of the Symposium in Celebration of the Work of
C.A.R. Hoare, Oxford, 13-15 September, 1999.
[C102]. Shuzhen Dong, Qiwen Xu
and Naijun Zhan (1999): A formal proof of the rate monotonic scheduler. In the Proc. of RTCSA 1999. IEEE Computer Society
Press.
Invited
talks:
·
Connecting algebraical and logical descriptions of concurrent
systems, TAMC 2005, Kunming.
·
Program verification by reduction to semi-algebraic system
solving, SCTC 2008, Shanghai.
·
An assume/guarantee based compositional calculus for Hybrid
CSP, TAMC 2012, Beijing.
·
Formal verification of Simulink diagrams, PAS 2013, Beijing.
·
Formal modelling, analysis and verification of hybrid
systems, tutorial of ICTAC 2013,
Shanghai.
·
Formal modelling, analysis and verification of hybrid
systems, tutorial of FACS 2013,
Nanchang.
·
Formal verification of Simulink/Stateflow
diagrams, tutorial of ESWEEK 2014,
New Delhi.
·
Model-checking of extended linear duration invariants, ProCoS workshop, London, 2015.
·
Formal verification of stochastic differential equations, Workshop on Quantitative Model Checking,
Singapore, 2016.
·
Invariant-based verification and synthesis for hybrid
systems, IFIP Working Group 2.2
Scientific Meeting, Singapore, 2016.
·
Formal design of embedded systems, IFIP Working Group 1.9/2.15 & Working Group 2.3 Annual Meeting,
Montaubon, France, 2016.
·
Invariant-based verification and synthesis for hybrid systems, Summer School on Symbolic Computation, Nanning, Jul. 16-22, 2017
·
Automatically generating SystemC
code from HCSP formal models, SATE 2017, Harbin, 2017
·
Automatically generating SystemC code from delay HCSP, APLAS 2017, Suzhou, 2017
·
Automatically generating SystemC
code from HCSP formal models, MAVoLS 2017,
Beijing, 2017
·
Taming Delays in Cyber-Physical Systems, ICFEM 2019, Shenzhen, China, Nov. 5-9 2019.
·
Practical Verification of Intelligent CPSs, ICMS 2020, TU
Braunschweig, Germany, July 13-16, 2020.
·
Non-linear interpolant
generation and its application to program verification, FROM 2020, Babes-Bolyai
University, Romania, Sept. 4-6,
2020.
·
Formal Analysis, Verification and Design of Safety-Critical
CPS, RTSS 2020, Houston, USA, Dec. 1st-4th,
2020.
·
Taming Delays in Cyber-Physical Systems, ICTAC 2020, MACAU, China, Nov. 30-Dec.4, 2020.
·
Invariant Generation by Constraint Solving in Verification of
Programs and Hybrid, TASE 2020, Hangzhou, China, Dec. 11-13,
2020.
·
Extending Hoare Logic to Hybrid Systems, VSTE 2021, Isaac Newton Institute,
Cambridge University, Jun. 7-11, 2021.
·
Extending Hoare Logic to Hybrid Systems, VSTE 2021, Isaac Newton Institute,
Cambridge University, Jun. 7-11, 2021.
·
Taming Delays in Cyber-Physical Systems, VSTE
2022, Isaac Newton Institute, Cambridge University, Jul. 21-28, 2022.
· Reset Controller Synthesis by Computing Invariants and Reach-avoid Sets, TASE 2023, 4-6 July 2023, Bristol, United Kingdom.
·
Synthesizing (Differential)
Invariants by Reduction Non-Convex Programming to SDP, ICFEM 2024, 2 ~ 6 December 2024 - Hiroshima, Japan.
Last modified: Jan. 30, 2023