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, book chapters and edited volumes:**

[B1]. Chaochen Zhou and Naijun Zhan: **Introduction to Formal
Semantics**, Academic Press. 2017. (in Chinese)

[B2]. Naijun Zhan,** **Shuling Wang and Hengjun Zhao:** Formal Verification of Simulink/Stateflow Diagrams**

[B3]. 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, 2016, ISBN 978-3-319-47676-6. (Editor)

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

[B5]. MengfeiYang and Naijun Zhan: *Combining Formal and Informal
Methods in the Design of Spacecrafts*. In SETSS 2014, ** Lecture
Notes in Computer Science** 9506, Springer-Verlag. 2016.

[B6]. Naijun Zhan, Shuling Wang and Hengjun Zhao: *Formal Modelling, Analysis and
Verification of Hybrid Systems*. In the Theories of Programming, ** Lecture
Notes in Computer Science** 8050, Springer-Verlag. 2013.

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

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

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

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

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

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

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

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

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

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

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

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

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

**Peer-reviewed Conferences and Workshops:**

[C1]. Lingtai Wang, Naijun Zhan and Jie An (2018): *The opacity of real-time automata*. In Proc. of EMSOFT 2018. (Also appear in
the special issue of IEEE TCAD for EMSOFT 2018, see [J1])

[C2]. Mingshuai Chen, Martin Fraenzle, Yangjia Li, Peter N.
Mosad 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****
10606**.

[C3]. Lingtai Wang and Naijun Zhan (2018): *Decidability of the initial-state opacity
of real-time automata*. In Prof. Chaochen Zhou’s Festschrift, **Lecture Notes in
Computer Science****.**

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Last
modified: Jul. 22, 2017