您现在的位置: 首页 » 师资队伍 » 教研系列 » 按研究所 » 软件研究所 » 正文

师资队伍

软件研究所

詹乃军

职称:教授

研究所:软件研究所

研究领域:计算机软件与理论

电子邮件:njzhanpku.edu.cn

个人主页://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.