个人主页：//lcs.ios.ac.cn/~znj/
主要研究方向
信息物理融合系统设计
程序验证
模态和时序逻辑
主要科研项目（在研）
1. “安全攸关软件框架验证的数学方法与应用”项目，国家重点研发计划，科技部，项目负责人，2022.11-2027.10，1490万
2. “面向嵌入式系统的软件IP知识建模与构造”项目，国家基金委重大项目，课题负责人，2022.1-2026.12，320万
3. “东风微内核操作系统形式化验证”项目，航天科工四院重大型号项目，项目负责人，2021.10-2023.12,1750万
4. “国际杰出团队”项目，中国科学院，项目负责人，2024.1-2026.12，300万
主要学术任职
中国计算机学会形式化方法专委会主任
国际会议SETTA及MEMOCODE指导委员会成员
国际杂志Journal of Automated Reasoning 、Formal Aspects of Computing,、Journal of Logical and Algebraic Methods in Programming 、Research Direction: Cyber-Physical Systems等编委，以及国内杂志《软件学报》、《电子学报》、《计算机研究与发展》、《信息安全学报》、《计算机科学》、《前瞻科技》等编委
国际会议程序委员会委员，如CAV、RTSS、EMSOFT、HSCC、FM、TACAS、ICCPS、IFM等。
Selected Publications
[1] Chaochen Zhou and Naijun Zhan (2017): Introduction to Formal Semantics, Academic Press. (in Chinese)
[2] Naijun Zhan, Shuling Wang and Hengjun Zhao (2016): Formal Verification of Simulink/Stateflow Diagrams, Springer-Verlag.
[3] Bai Xue, Naijun Zhan and Martin Fränzle (2023): Reach-Avoid Analysis for Stochastic Differential Equations. IEEE Transactions on Automatic Control, 10.1109/TAC.2023.3332570, in press.
[4] 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.
[5] 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.
[6] 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
[7] 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 (full version of CAV 2021 paper)
[8] X. Xu, B. Zhan, S. Wang, J.-P. 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, https://doi.org/10.1145/3517192.
[9] X. Xu, B. Zhan, S. Wang, X. Jin, J.-P. 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.
[10] 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.
[11] 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.
[12] 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
[13] 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.
[14] 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)
[15] 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.
[16] 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.
[17] 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)
[18] 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.
[19] 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)
[20] 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.
[21] 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)
[22] 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.
[23] Liyun Dai, Ting Gan, Bican Xia and Naijun Zhan (2017): Barrier certificate revisited. Journal of Symbolic Computation, 80:62-86.
[24] 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.
[25] Naijun Zhan and Mila Majster-Cederbaum (2010): On hierarchically developing reactive systems. Information and Computation, 208(9):997-1019.
[26] Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, and Naijun Zhan (2024): Formally Verified C Code Generation from Hybrid Communicating Sequential Processe. Accepted by ICCPS 2024.
[27] Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan and Joost-Pieter Katoen (2021): Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. In Proc. of CAV 2021, Lecture Notes in Computer Science 12759, pp.443-466.
[28] 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.
[29] 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.
[30] 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.
[31] 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.
[32] 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.
[33] 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.
[34] 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.
[35] 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.
[36] 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.
[37] 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.
[38] 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)
[39] 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)
[40] 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.
[41] 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.
[42] Bai Xue, Martin Fraenzle and Naijun Zhan (2018): Under-Approximating Reach Sets for Polynomial Continuous Systems. In Proc. of HSCC 2018, pp.51-60.
[43] 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.
[44] 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.
[45] 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.
[46] 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.
[47] 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.
[48] Naijun Zhan and Liang Zou (2014): Formal verification of Simulink/Stateflow diagrams, in Proc. of ESWEEK 2014 (abstract 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.
[49] 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.
[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] Computing semi-algebraic invariants for polynomial dynamical systems, in Proc. of EMSOFT 2011, pp.97-106, ACM Press.
