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 (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)

[J32]. Yang Gao, Ming Xu, Naijun
Zhan and Lijun Zhang (2013): ** Model-checking Conditional CSL for
Continuous-time Markov Chains**.

[J33]. Jiang Liu, Naijun Zhan, and Hengjun Zhao (2012): ** Automatically
discovering relaxed Lyapunov functions for polynomial dynamical systems**.

[J34]. Bican Xia, Lu Yang, Naijun
Zhan and Zhihai Zhang (2011): ** Symbolic
decision procedure for termination**.

[J35]. Qiwen Xu and Naijun
Zhan (2010): ** Rate Monotonic Scheduling Re-analyzed**.

[J36]. Naijun Zhan (2010):** **** Connection between algebraical and logical
approaches to concurrent systems**.

[J37]. Yang Lu, Chaochen Zhou, Naijun Zhan and Bican Xia (2010):
** Recent advances in program verification through
computer algebra**.

[J38]. Naijun Zhan and Mila Majster-Cederbaum
(2010):** **** On
hierarchically developing reactive systems**.

[J39]. Zhenbang Chen, Zhiming
Liu, Volker Stolz, Anders P. Ravn, and Naijun Zhan (2009):** **** Refinement
and verification in component based and model driven design**.

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

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

[J42]. Naijun Zhan (2004): ** Compositional
properties of sequential processes**.

[J43]. Naijun Zhan (2001): ** A
higher-order duration calculus and its completeness**.

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

**Peer-reviewed Conferences and Workshops:**

[C1]. Han Su, Shenghua Feng, Sinong Zhan and Naijun Zhan
(2024): ** Switching Controller Synthesis for Hybrids Systems
Against STL Formulas**. Accepted by

[C2]. 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**. Accepted by

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

[C4]. Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan and
Ichiro Hasuo (2024): ** The
Opacity of Timed Automata**. Accepted by

[C5]. Chenhao Wu, Ruoxiang Li,
Naijun Zhan and Nan Guan (2024): ** Improving
the Reaction Latency Analysis of Message Synchronization in ROS**. Accepted by

[C6]. 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****). **Accepted by

[C7]. Shicheng Yi, Shuling
Wang, Bohua Zhan and Naijun
Zhan (2022):** **** An Executable Semantics for Stateflow in
Isabelle/HOL**. In Proc. of

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

[C9]. Bai Xue, Qiuye
Wang, Naijun Zhan, Martin Frnzle,
Shenghua Feng (2022): ** Differential Games Based on Invariant Sets
Generation**. In Proc. of

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

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

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

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

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

[C15]. Bai Xue, Renjue
Li, Naijun Zhan, Martin Fränzle (2021): ** Reach-avoid Analysis for Stochastic
Discrete-time Systems**. In Proc. of

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

[C17]. Bai Xue and Naijun Zhan (2020): ** Probably Approximately Correct Interpolants
Generation**. In Proc. of

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

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

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

[C21]. Shenghua Feng, Mingshuai Chen, Sriram Sankaranarayanan, Bai Xue and Naijun Zhan (2020):** Unbounded-time
Safety Verification of Stochastic Differential Dynamics**. In Proc. of

[C22]. Ting Gan, Bican
Xia, Bai Xue, Naijun Zhan
and Liyun Dai (2020): ** Non-linear
Interpolant Generation**. In Proc. of

[C23]. Bai Xue, Naijun Zhan and Yangjia Li
(2020):**
Robust Regions of Attraction Generation for State-Constrained Perturbed
Discrete-Time Polynomial Systems**. In Proc. of

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

[C25]. Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan and Miaomiao Zhan (2020): ** Learning
one-clock timed automata**. In Proc. of

[C26]. Naijun Zhan (2019): ** Taming
delays in cyber-physical systems**. In Proc. of

[C27]. Bai Xue, Martin Fraenzle, Hengjun Zhao, Naijun Zhan and Arvind Easwaran (2019): ** Probably
Approximate Safety Verification of Hybrid Dynamical Systems**. In Proc. of

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

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

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

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

[C32]. Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur and Naijun Zhan (2019): ** NIL:
Learning Nonlinear Interpolants**. In Proc. of

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

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

[C35]. Lingtai Wang, Naijun
Zhan and Jie An (2018): ** The
opacity of real-time automata**. In Proc. of

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

[C37]. Bai Xue, Naijun
Zhan, Yangjia Li and Qiuye
Wang (2018): ** Robust Non-termination Analysis of
Numerical Software**. In Proc. of

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

[C39]. Yijun Feng, Joost-Pieter Katoen,
Haokun Li, Bican Xia and Naijun Zhan (2018): ** Monitoring
CTMCs by multi-clock timed automata**. In Proc. of

[C40]. Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang and Wang Yi (2018): ** Model-checking continuous-time bounded
extended linear duration invariants**. In
Proc. of

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

[C42]. Dimitar P. Guelev, Shuling Wang, Naijun Zhan
(2017): ** Compositional Hoare-Style Reasoning About
Hybrid CSP in the Duration Calculus**. In Proc. of

[C43]. Gaogao Yan, Li Jiao, Shuling
Wang and Naijun Zhan (2017): ** Generating
SystemC code from delay HCSP**. In Proc. of

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

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

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

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

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

[C49]. Ting Gan, Mingshuai Chen, Yangjia
Li, Bican Xia and Naijun
Zhan (2016): ** Computing reachable sets of linear vector
fields revisited**, in Proc. of

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

[C51]. Yu Peng, Shuling Wang, Naijun
Zhan, Lijun Zhang (2015): ** Extending
Hybrid CSP with Probability and Stochasticity**, in Proc.

[C52]. S. Wang, N. Zhan and L. Zou (2015): ** An
improved HHL prover: An interactive theorem prover for hybrid systems**, in Proc. of

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

[C54]. Liang Zou, Naijun Zhan, Shuling Wang and Martin Fraenzle
(2015): ** Formal verification of Simulink/Stateflow
diagrams**, in Proc. of

[C55]. Liang Zou, Martin Fraenzle, Naijun Zhan and Peter Nazier Mosaad (2015): ** Automatic
stability and safety verification for delay differential equations**, in Proc. of

[C56]. Jiang Liu, Naijun Zhan, Hengjun Zhao and Liang Zou (2015): ** Abstraction
of elementary hybrid systems by variable transformation**, in Proc. of FM 2015,

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

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

[C59]. Ehsan Ahmad, Yunwei Dong, Shuling Wang, Naijun Zhan and
Liang Zou (2014): ** Adding Formal Meanings to AADL Models with
Hybrid Annex**, in Proc. of

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

[C61]. Ruzhen Dong and Naijun
Zhan (2013): ** Towards a failure model of software
components**, in Proc. of

[C62]. Dimitar P. Guelev, Shuling Wang, Naijun
Zhan and Chaochen Zhou (2013): ** Super-dense
computation in verification of HCSP processes**, in Proc. of

[C63]. Liang Zou, Naijun Zhan, Shuling Wang, Martin Fraenzle and
Shengchao Qin (2013): ** Verifying
Simulink diagrams via a Hybrid Hoare Logic prover**, in Proc. of

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

[C65]. Yang Gao, Ernst Moritz Hahn, Naijun
Zhan and Lijun Zhang (2013): ** A
CSL model checker for continuous-time markov chains**, in Proc. of

[C66]. Ruzhen Dong, Naijun
Zhan and Liang Zhao (2013): ** An
interface model of software components**, in Proc. of

[C67]. Hengjun Zhao, Naijun
Zhan and Deepak Kapur (2013): ** Synthesizing
switching controllers for hybrid systems by generating invariants**, in Proc. of

[C68]. Liyun Dai, Bican Xia
and Naijun Zhan (2013): ** Generating
non-linear interpolants by semi-definite programming**, in Proc. of

[C69]. Quan Zu, Miaomiao
Zhang, Jiaqi Zhu and Naijun
Zhan (2013): ** Bounded model-checking of discrete Duration
Calculus**, in
Proc. of

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

[C71]. Shuling Wang, Naijun
Zhan and Dimitar Guelev
(2012): ** An assume/guarantee based compositional
calculus for Hybrid CSP**. A keynotes of

[C72]. Ruzhen Dong, Johannes Farber, Zhiming
Liu, Jiri Srba, Naijun Zhan,
and Jiaqi Zhu (2012): ** Unblockable
compositions of software components**, in Proc. of

[C73]. Jiang Liu, Naijun Zhan and Hengjun Zhao (2011):** Computing
semi-algebraic invariants for polynomial dynamical systems**, in Proc. of

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

[C75]. ZizhenWang, HanpinWang and Naijun Zhan (2010): ** Refinement
theories of software components**.

[C76]. Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou and
Liang Zou (2010): ** A
calculus for HCSP**. A keynotes of

[C77]. Miaomiao Zhang, Zhiming
Liu and Naijun Zhan (2009): ** Model
checking linear duration invariants of networks of automata**. In Proc.

[C78]. Naijun Zhan, Eoun-Yound
Kang and Zhiming Liu (2008): ** Refinement
and composition of components in rCOS**. In Proc. of

[C79]. Bican Xia, Lu Yang and Naijun
Zhan (2008): ** Program verification by reduction to
semi-algebraic systems solving**, in Proc. of

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

[C81]. Xin Chen, Jifeng He, Zhiming Liu and Naijun Zhan
(2007): ** A model of compoent-based programming**. In Proc. Of

[C82]. Yinghua Chen, Bican Xia,
Lu Yang, and Naijun Zhan (2007):** **** Reducing
polynomial invariant generation to semi-algebraic systems solving**. In Proc. of

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

[C84]. Naijun Zhan (2006):** **** Connecting algebraical and logical
descriptions of concurrent systems**. In the Proc. of

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

[C86]. Naijun Zhan and Jinzhao
Wu (2005): ** Compositionality of fixpoint logic with chop**. In the Proc. of

[C87]. 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 (

[C88]. Lu Yang, Naijun Zhan, Bican Xia and Chaochen Zhou
(2005): ** Program verification by using DISCOVERER**. In the Proc. of

[C89]. Mila Majster-Cederbaum, Jinzhao Wu, Houguang Yue, Naijun Zhan (2004): *Refinement
of actions for real-time concurrent systems with causal ambiguit**y*. In the Proc. of **ICFEM 2004**, **Lecture Notes in
Computer Science** 3308, pp. 449-463.

[C90]. Naijun Zhan (2003): ** Combining
hierarchical specification with hierarchical implementation**. In the Proc. of

[C91]. M. Majster-Cederbaum, Naijun Zhan and Harald Fecher
(2003): ** Action refinement from a logical point of
view**. In the Proc. of

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

[C93]. Naijun Zhan (2000): ** Completeness
of higher-order duration calculus**. In the proc. of

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

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

[C96]. 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: Jan. 30, 2023