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

[1]. Naijun Zhan, Shuling Wang and Hengjun Zhao: Formal Verification of Simulink/Stateflow Diagrams, Springer-Verlag. 2017.

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

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

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

Journals:

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

[6]. 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. (full version of SETTA 2015)

[7]. Shuling Wang, Flemming Nielson, Hanne Riis Nielson and Naijun Zhan (2016): Modelling and Verifying Communication Failure of Hybrid Systems in HCSP. Computer Journal, DOI:https://doi.org/10.1093/comjnl/bxw084

[8]. Liyun Dai, Ting Gan, Bican Xia and Naijun Zhan (2015): Barrier certificate revisited. Journal of Symbolic Computation, 80:62-86.

[9]. 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 Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL. Science China Information Sciences, 58(11):1-20.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

 

Peer-reviewed Conferences and Workshops:

 

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

[26]. Bai Xue, Peter Nazier Mosaad, Martin Fraenzle, Mingshuai Chen, Yangjia Li and Naijun Zhan (2017): Safe over- and under-approximation Safe over- and under-approximation of reachable sets for delay differential equationsof reachable sets for delay differential equations, in Proc. of FORMATS 2017, Lecture Notes in Computer Science.

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

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

[29]. Mingshuai Chen, Xiao Han, Tao Tang, Shuling Wang, Mengfei Yang, Naijun Zhan, Hengjun Zhao and Liang Zou (2016): MARS: A toolchain for modeling, analysis and verification of hybrid systems, in Proc. of ProCoS 2015. 

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

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

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

[33]. Yu PengShuling 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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


Naijun Zhan

Last modified: Jul. 22, 2017

hit counter joomla