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**

[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,

[B5]. Naijun Zhan, Shuling Wang and Hengjun Zhao (2013): **Formal Modelling, Analysis and
Verification of Hybrid Systems**. In the Theories of Programming,

[E1]. 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)

[E2]. 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)

[E3]. 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)

[E4]. 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)

[E5]. Martin Fränzle, Deepak Kapur, Heike Wehrheim, Naijun Zhan (2019): ** Formal
Aspects Comput. **31(1), special issue on SETTA 2016.

[E6]. Arvind Easwaran, Qi Zhu, Naijun Zhan (2020): ** Journal
of Systems Architecture**, special Issue on ICESS 2019

[E7]. Naijun Zhan, Xuandong Li and Ji Wang (2016): ** Journal
of Software **27(3), special issue on formal methods and its
application. (in Chinese)

[J28]. 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.

[J29]. 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.

[J30]. 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.

[J31]. 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

[J32]. Naijun Zhan (2010): *Connection between algebraical and logical
approaches to concurrent systems*. **Mathematical
Structures in Computer Science**, 20(5):915-950.

[J33]. 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.

[J34]. Naijun Zhan and Mila Majster-Cederbaum
(2010):** ***On hierarchically developing reactive
systems*. **Information
and Computation**, 208(9):997-1019.

[J35]. 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.

[J36]. Xu Qiwen and Naijun Zhan (2008):** ***Formalizing scheduling theorems using
duration calculus*. **Nordic
Journal of Computing**, 14:173- 201.

[J37]. 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.

[J38]. Naijun Zhan (2004): *Compositional properties of sequential
processes*. **Electronic
Notes in Theoretical Computer Science**, 118:111-128.

[J39]. Naijun Zhan (2001): *A higher-order duration calculus and its
completeness*. **Science China**,
Vol 30(5).

[J40]. Naijun Zhan (2001): *An intuitive proof for DDS*. **Journal
of Computer Science and Technology**, 16(2):146-158.

**Peer-reviewed Conferences and Workshops:**

[C1]. Shicheng Yi, Shuling
Wang, Bohua Zhan and Naijun
Zhan (2022): *An
Executable Semantics for Stateflow in Isabelle/HOL*. Accepted by ICFEM 2022.

[C2]. Xiaochen Tang, Wei Shen, Miaomiao
Zhang, Jie An, Bohua Zhan
and Naijun Zhan (2022): *Learning Deterministic One-Clock Timed
Automata via Mutation Testing*. Accepted by ATVA 2022.

[C3]. 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

[C4]. 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.

[C5]. Bai Xue, Yunjun
Bai, Naijun Zhan, Wenyou
Liu and Li Jiao (2021): *Reach-Avoid Analysis for Delay Differential
Equations*. CDC 2021, pp.1301-1307.

[C6]. Jie An, Bohua Zhan, Naijun Zhan and Miaomiao Zhang
(2021):** ***Learning
Nondeterministic Real-Time Automata***.** Accepted by EMSOFT 2021.

[C7]. 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.

[C8]. 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.

[C9]. 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.

[C10]. 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.

[C11]. 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.

[C12]. 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.

[C13]. 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.

[C14]. 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**.

[C15]. 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.

[C16]. 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.

[C17]. 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.

[C18]. 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.

[C19]. 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.

[C20]. 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)

[C21]. 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.

[C22]. 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

[C23]. 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.

[C24]. 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.

[C25]. 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.

[C26]. 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.

[C27].
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.

[C28]. 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

[C29]. 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)

[C30]. 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**)

[C31]. 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**)

[C32]. 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 80^{th} Birthday, **Lecture Notes in Computer Science 11180**, pp. 40-60.

[C33]. 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.

[C34]. 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.

[C35]. Bai Xue, Martin Fraenzle and Naijun Zhan (2018): *Under-Approximating Reach Sets for
Polynomial Continuous Systems*** .** In Proc. of HSCC 2018, pp.51-60.

[C36]. 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.

[C37]. 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.

[C38]. 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.

[C39]. 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**)

[C40]. 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.

[C41]. 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.

[C42]. 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.

[C43]. 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.

[C44]. 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.

[C45]. 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.

[C46]. 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.

[C47]. 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.

[C48]. 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.

[C49]. 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.

[C50]. 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.

[C51]. Naijun Zhan and Liang Zou (2014): *Formal verification of Simulink/Stateflow diagrams*, in Proc. of **ESWEEK 2014** (abstract only).

[C52]. 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.

[C53]. 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.

[C54]. 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.

[C55]. 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.

[C56]. 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.

[C57]. 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.

[C58]. 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.

[C59]. 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.

[C60]. 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.

[C61]. 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.

[C62]. 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.

[C63]. 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.

[C64]. 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.

[C65]. 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.

[C66]. 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.

[C67]. 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.

[C68]. 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.

[C69]. ZizhenWang, HanpinWang and Naijun Zhan (2010): *Refinement theories of software components*. **ACM
SIGAPP SAC 2010**, pp.2311-2318.

[C70]. 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.

[C71]. 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.

[C72]. 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.

[C73]. 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.

[C74]. 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.

[C75]. 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.

[C76]. 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.

[C77]. 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.

[C78]. Naijun Zhan (2006): *Connecting algebraical and logical
descriptions of concurrent systems*. In the Proc. of **ISoLA**** 2006**, IEEE Computer Society Press.

[C79]. 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.

[C80]. 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.

[C81]. 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.

[C82]. 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.

[C83]. 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.

[C84]. Naijun Zhan (2003): *Combining hierarchical specification with hierarchical
implementation*. In the Proc. of **ASIAN 2003**, **Lecture Notes in
Computer Science** 2896, pp. 110-124.

[C85]. 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.

[C86]. 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.

[C87]. Naijun Zhan (2000): *Completeness of higher-order duration
calculus*. In the proc. of **CSL 2000**,** Lecture Notes in Computer Science **1863.

[C88]. Naijun Zhan: *Another
formal proof for deadline driven scheduler*. In the Proc. of RTCSA'00, IEEE
Computer Society Press.

[C89]. 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.

[C90]. 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.

·
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. 1^{st}-4^{th},
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.

Last modified: Jul. 22, 2017