基本信息
詹乃军  男  博导  中国科学院软件研究所
电子邮件: znj@ios.ac.cn
通信地址: 北京中关村南四街4号,8718信箱
邮政编码: 100190

研究领域

实时和混成系统、信息物理融合系统、形式化方法、计算语义模型、程序验证

招生信息

博士一名,硕士一名
招生专业
081202-计算机软件与理论
083500-软件工程
招生方向
信息物理融合系统
程序理论与验证技术
软件工程

教育背景

1997-09--2000-07   中科院软件所   博士
1993-09--1996-06   南京大学计算机科学与技术系   硕士
1989-09--1993-06   南京大学数学系   学士
学历
-- 研究生
学位
-- 博士
出国学习工作
•2011.12.1—2011.12.15: 丹麦工业大学计算机系,访问教授;
•2011.2.12—2011.3.7: 美国新墨西哥大学计算机系,访问教授;
•2010.7.30—2010.8.13: 新加坡南洋科技大学,访问教授;
•2006.9—2006.11,2007.9—2007.11,2009.8—2009.10:三次访问联合国大学国际软件技术研究所,高级访问学者;
•2008.10.17—2008.10.31,2009.7.25—2009.8.7:两次访问保加利亚科学院数学和信息研究所,访问教授;
•2001.5—2004.7: 德国曼海姆大学数学和计算机科学学院实用信息第二研究所,助理研究员;
•2000.5—2000.7: 联合国大学国际软件技术研究所,访问学者;
•1998.7—1999.10: 联合国大学国际软件技术研究所,做博士论文;

工作经历

   
工作简历
2016-01~现在, 中国科学院, 特聘研究员
2015-03~现在, 中国科学院大学, 岗位教授
2008-10~现在, 中科院软件所, 研究员
2004-09~2008-09,中科院软件所, 副研究员
2001-05~2004-07,德国曼海姆大学, 助理研究员
社会兼职
2020-01-01-今,中国计算机学会形式化方法专业委员会, 副主任
2016-01-01-今,Journal of Logical and Algebraic Methods in Programming, 编委
2015-03-01-今,《Formal Aspects of Computing》编委,
2015-01-01-今,《软件学报》编委,
2015-01-01-今,FME Awards Committee,
2014-03-01-今,《计算机研究与发展》编委,

教授课程

本科生毕业设计(计算机科学与技术)
离散数学
数理逻辑与程序理论
模态和时序逻辑
混成系统建模和验证

专利与奖励

   
奖励信息
(1) 航天嵌入式软件可信保障关键技术和应用, 一等奖, 省级, 2019
(2) 实时和嵌入式系统形式设计理论, 三等奖, 省级, 2018

出版信息

   
发表论文
[1] 薛白, 詹乃军, 王戟, 刘万伟. Reach-avoid Verification Based on Convex Optimization. IEEE Transactions on Automatic Control (IEEE TAC)[J]. 2023, [2] Xu, Xiong, Talpin, JeanPierre, Wang, Shuling, Zhan, Bohua, Zhan, Naijun. Semantics Foundation for Cyber-physical Systems Using Higher-order UTP. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY[J]. 2023, 32(1): http://dx.doi.org/10.1145/3517192.
[3] Bai Xue, 詹乃军, Martin Fraenzle. Reach-Avoid Analysis for Stochastic Differential Equations. IEEE TRANSACTIONS ON AUTOMATIC CONTROL[J]. 2023, [4] Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, 詹乃军. Lower Bounds for Possibly Divergent Probabilistic Programs. OOPSLAnull. 2023, [5] Liu, Wenyou, Bai, Yunjun, Jiao, Li, Zhan, Naijun. Safety guarantee for time-delay systems with disturbances. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2023, 66(3): 114-128, [6] Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, 詹乃军. A Decision Procedure for String Constraints with String-Integer Conversion and Flat Regular Constraints. Acta Informatica[J]. 2023, [7] Xu, Xiong, Zhan, Bohua, Wang, Shuling, Talpin, JeanPierre, Zhan, Naijun. A denotational semantics of Simulink with higher-order UTP. JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING[J]. 2023, 130: http://dx.doi.org/10.1016/j.jlamp.2022.100809.
[8] Bai Xue, Qiuye Wang, 詹乃军, Martin Fraenzle, Shenghua Feng. Differential Games Based on Invariant Sets Generation. 2022 American Control Conference (ACC)null. 2022, [9] Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, 詹乃军. Learning Deterministic One-Clock Timed Automata via Mutation Testing. ATVA 2022null. 2022, [10] Shicheng Yi, Shuling Wang, Bohua Zhan, 詹乃军. An Executable Semantics for Stateflow in Isabelle/HOL. ICFEM 2022null. 2022, [11] Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan. Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow. Theoretical Computer Science[J]. 2022, 903: 1-25, [12] Yang, Tengshun, Wang, Shuling, Zhan, Bohua, Zhan, Naijun, Li, Jinghui, Xiang, Shuangqing, Xiang, Zhan, Mao, Bifei. Formal Analysis of 5G Authentication and Key Management for Applications (AKMA). JOURNAL OF SYSTEMS ARCHITECTURE[J]. 2022, 126: http://dx.doi.org/10.1016/j.sysarc.2022.102478.
[13] Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan. Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP. ACM Trans. Softw. Eng. Methodol.[J]. 2022, 1-47, [14] Qiuye Wang, Mingshuai Chen, Bai Xue, 詹乃军, Joost-Pieter Katoen. Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming. Information and Computation[J]. 2022, [15] Xue, Bai, Zhan, Naijun. Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems. IEEE TRANSACTIONS ON AUTOMATIC CONTROL[J]. 2022, 67(2): 1053-1060, [16] Xue, Bai, Zhan, Naijun, Frnzle, Martin. Reach-Avoid Analysis for Stochastic Differential Equations. 2022, http://arxiv.org/abs/2208.10752.
[17] Jie AN, Lingtai WANG, Bohua ZHAN, Naijun ZHAN, Miaomiao ZHANG. Learning real-time automata. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2021, 64(9): 53-69, [18] Chen, Mingshuai, Fraenzle, Martin, Li, Yangjia, Mosaad, Peter N, Zhan, Naijun. Indecision and delays are the parents of failure-taming them algorithmically by synthesizing delay-resilient control. ACTA INFORMATICA[J]. 2021, 58(5): 497-528, [19] 詹乃军. Reach-Avoid Analysis for Delay Differential Equations. CDC. 2021, [20] Jin, Xiangyu, An, Jie, Zhan, Bohua, Zhan, Naijun, Zhan, Miaomiao. Inferring Switched Nonlinear Dynamical Systems. FORMAL ASPECTS OF COMPUTING[J]. 2021, 33(3): 385-406, http://dx.doi.org/10.1007/s00165-021-00542-7.
[21] 詹乃军. Reach-avoid Analysis for Stochastic Discrete-time Systems. ACC. 2021, [22] Wang, Qiuye, Chen, Mingshuai, Xue, Bai, Zhan, Naijun, Katoen, JoostPieter. Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. 2021, http://arxiv.org/abs/2105.14311.
[23] 詹乃军. 时延混成系统的切换控制器合成. 中国科学 数学. 2021, [24] 詹乃军. Safety Guarantee for Time-Delay Systems with Disturbances by Control Barrier Functionals. Science China Information Science. 2021, [25] 詹乃军. Switching Controller Synthesis for Time-delayed Hybrid Systems under Perturbation. HSCC. 2021, [26] Zhan, Bohua, Gu, Bin, Xu, Xiong, Jin, Xiangyu, Wang, Shuling, Xue, Bai, Li, Xiaofeng, Chen, Yao, Yang, Mengfei, Zhan, Naijun. Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. 2021 IEEE 27TH REAL-TIME AND EMBEDDED TECHNOLOGY AND APPLICATIONS SYMPOSIUM (RTAS 2021)[J]. 2021, 457-460, [27] Xue, Bai, Wang, Qiuye, Zhan, Naijun, Wang, Shijie, She, Zhikun. Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang and Zhikun She. Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. SIAM JOURNAL ON CONTROL AND OPTIMIZATION[J]. 2021, 59(2): 1083-1108, http://dx.doi.org/10.1137/19M125220X.
[28] Wang, Qiuye. Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan and Joost-Pieter Katoen. Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. In Proceedings of the 33rd International Conference on Computer-Aided Verification[J]. 2021, [29] An, Jie, Zhan, Bohua, Zhan, Naijun, Zhang, Miaomiao. Learning Nondeterministic Real-Time Automata. ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS[J]. 2021, 20(5): http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000699999600050.
[30] Xue, Bai, Wang, Qiuye, Feng, Shenghua, Zhan, Naijun. Bai Xue, Qiuye Wang, Shenghua Feng and Naijun Zhan. Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations. IEEE TRANSACTIONS ON AUTOMATIC CONTROL[J]. 2021, 66(1): 283-290, https://www.webofscience.com/wos/woscc/full-record/WOS:000603044900021.
[31] Xue, Bai, Zhan, Naijun, Li, Yangjia. Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems. 2020, http://arxiv.org/abs/1810.11767.
[32] Yan, Gaogao, Jiao, Li, Wang, Shuling, Wang, Lingtai, Zhan, Naijun. Automatically Generating SystemC Code from HCSP Formal Models. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY[J]. 2020, 29(1): [33] Bai Xue, Naijun Zhan, Yangjia Li. A Characterization of Robust Regions of Attraction for Discrete-Time Systems Based on Bellman Equations. IFAC PAPERSONLINE. 2020, 53(2): 6390-6397, [34] 詹乃军. Over- and Under-Approximating Reach Sets for Perturbed Delay Differential Equations. IEEE Transaction on Automatic Control. 2020, [35] 詹乃军. Probably Approximately Correct Interpolants Generation. SETTA 2020, LNCS 12153. 2020, [36] 詹乃军. Inner-approximating reach-avoid sets for discrete-time polynomial systems. CDC 2020. 2020, [37] Xue, Bai, Wang, Qiuye, Zhan, Naijun, Wang, Shijie, She, Zhikun. Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. 2020, http://arxiv.org/abs/1812.10588.
[38] 詹乃军. Non-linear Interpolant Generation.. CAV 2020. 2020, [39] Xue, Bai, Fraenzle, Martin, Zhan, Naijun. Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties. IEEE TRANSACTIONS ON AUTOMATIC CONTROL[J]. 2020, 65(4): 1468-1483, https://www.webofscience.com/wos/woscc/full-record/WOS:000522918700008.
[40] Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Learning One-Clock Timed Automata. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS[J]. 2020, 12078: 444-462, https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7439748/.
[41] Xue, Bai, Fraenzle, Martin, Zhan, Naijun, Bogomolov, Sergiy, Xia, Bican. Safety Verification for Random Ordinary Differential Equations. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS[J]. 2020, 39(11): 4090-4101, https://www.webofscience.com/wos/woscc/full-record/WOS:000587712700078.
[42] Feng, Shenghua, Chen, Mingshuai, Xue, Bai, Sankaranarayanan, Sriram, Zhan, Naijun. Unbounded-Time Safety Verification of Stochastic Differential Dynamics. 2020, http://arxiv.org/abs/2006.01858.
[43] Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan. PAC learning of deterministic one-clock timed automata. ICFEM 2020[J]. 2020, [44] Wang, Jian, An, Jie, Chen, Mingshuai, Zhan, Naijun, Wang, Lulin, Zhang, Miaomiao, Gan, Ting. From model to implementation: a network algorithm programming language. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2020, 63(7): 201-217, http://lib.cqvip.com/Qikan/Article/Detail?id=7102354895.
[45] Xue, Bai, Wang, Qiuye, Zhan, Naijun, Franzle, Martin, ACM. Robust Invariant Sets Generation for State-Constrained Perturbed Polynomial Systems. PROCEEDINGS OF THE 2019 22ND ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (HSCC '19)null. 2019, 128-137, http://dx.doi.org/10.1145/3302504.3311810.
[46] 詹乃军. Probably Approximate Safety Verification of Hybrid Dynamical Systems. In Proc. of ICFEM 2019, Lecture Notes in Computer Science 11852. 2019, [47] Liu Junyi, Zhan Bohua, Wang Shuling, Ying Shenggang, Liu Tao, Li Yangjia, Ying Mingsheng, Zhan Naijun. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. COMPUTER AIDED VERIFICATION, CAV 2019, PT II[J]. 2019, 11562: 187-207, [48] Feng Shenghua, Chen Mingshuai, Zhan Naijun, Franzle Martin, Xue Bai, Dillig I, Tasiran S. Taming Delays in Dynamical Systems Unbounded Verification of Delay Differential Equations. COMPUTER AIDED VERIFICATION, CAV 2019, PT Inull. 2019, 11561: 650-669, [49] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报[J]. 2019, 30(1): 33-61, http://lib.cqvip.com/Qikan/Article/Detail?id=7001388128.
[50] 詹乃军. Unified Graphical Co-Modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow. In Proc. of UTP 2019, Lecture Notes in Computer Science 11885. 2019, [51] 詹乃军. Automatically generating SystemC code from HCSP formal mdoels. ACM Transaction on Software Engineering and Methodoloty. 2019, [52] Chen Mingshuai, Wang Jian, An Jie, Zhan Bohua, Kapur Deepak, Zhan Naijun. NIL: Learning Nonlinear Interpolants. 2019, http://arxiv.org/abs/1905.11625.
[53] Xue Bai, Frnzle Martin, Zhan Naijun. Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties. 2019, http://arxiv.org/abs/1811.01086.
[54] Gan, Ting, Chen, Mingshuai, Li, Yangjia, Xia, Bican, Zhan, Naijun. Reachability Analysis for Solvable Dynamical Systems. IEEE TRANSACTIONS ON AUTOMATIC CONTROL[J]. 2018, 63(7): 2003-2018, https://www.webofscience.com/wos/woscc/full-record/WOS:000436468200010.
[55] Xue, Bai, Fraenzle, Martin, Zhan, Naijun, Assoc Comp Machinery. Under-Approximating Reach Sets for Polynomial Continuous Systems. HSCC 2018: PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (PART OF CPS WEEK)null. 2018, 51-60, http://dx.doi.org/10.1145/3178126.3178133.
[56] 詹乃军. Model Checking Continuous-time Bounded Extended Linear Duration Invariants. HSCC 2018. 2018, [57] 詹乃军. What’s to come is still unsure: Synthesizing synthesizers resilient to delayed reaction. ATVA 2018. 2018, [58] Wang, Lingtai, Zhan, Naijun, An, Jie. The Opacity of Real-Time Automata. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS[J]. 2018, 37(11): 2845-2856, http://dx.doi.org/10.1109/TCAD.2018.2857363.
[59] Feng Yijun, Katoen JoostPieter, Li Haokun, Xia Bican, Zhan Naijun, Chockler H, Weissenbacher G. Monitoring CTMCs by Multi-clock Timed Automata. COMPUTER AIDED VERIFICATION (CAV 2018), PT Inull. 2018, 10981: 507-526, [60] Wang, Lingtai, Zhan, Naijun, Jones, C, Wang, J, Zhan, N. Decidability of the Initial-State Opacity of Real-Time Automata. SYMPOSIUM ON REAL-TIME AND HYBRID SYSTEMS: ESSAYS DEDICATED TO PROFESSOR CHAOCHEN ZHOU ON THE OCCASION OF HIS 80TH BIRTHDAYnull. 2018, 11180: 44-60, [61] Xue, Bai, Mosaad, Peter Nazier, Fraenzle, Martin, Chen, Mingshuai, Li, Yangjia, Zhan, Naijun, Abate, A, Geeraerts, G. Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2017)null. 2017, 10419: 281-299, [62] 詹乃军. Generating SystemC code from delay HCSP. APLAS. 2017, [63] Wang, Shuling, Zhan, Naijun, Zhang, Lijun. A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. FORMAL ASPECTS OF COMPUTING[J]. 2017, 29(4): 751-775, http://dx.doi.org/10.1007/s00165-017-0421-7.
[64] Wang, Qiuye, Li, Yangjia, Xia, Bican, Zhan, Naijun. Generating Semi-Algebraic Invariants for Non-Autonomous Polynomial Hybrid Systems. JOURNAL OF SYSTEMS SCIENCE & COMPLEXITY[J]. 2017, 30(1): 234-252, https://www.webofscience.com/wos/woscc/full-record/WOS:000397236700015.
[65] Wang Shuling, Nielson Flemming, Nielson Hanne Riis, Zhan Naijun. Modelling and Verifying Communication Failure of Hybrid Systems in HCSP. THE COMPUTER JOURNAL[J]. 2017, [66] Feng, Yijun, Zhang, Lijun, Jansen, David N, Zhan, Naijun, Xia, Bican, DSouza, D, Kumar, KN. Finding Polynomial Loop Invariants for Probabilistic Programs. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2017)null. 2017, 10482: 400-416, [67] Yan, Gaogao, Jiao, Li, Wang, Shuling, Zhan, Naijun, Chang, BYE. Synthesizing SystemC Code from Delay Hybrid CSP. PROGRAMMING LANGUAGES AND SYSTEMS (APLAS 2017)null. 2017, 10695: 21-41, [68] Wang, Qiuye, Li, Yangjia, Xia, Bican, Zhan, Naijun. Generating Semi-Algebraic Invariants for Non-Autonomous Polynomial Hybrid Systems. JOURNAL OF SYSTEMS SCIENCE & COMPLEXITY[J]. 2017, 30(1): 234-252, https://www.webofscience.com/wos/woscc/full-record/WOS:000397236700015.
[69] Dai, Liyun, Gan, Ting, Xia, Bican, Zhan, Naijun. Barrier certificates revisited. JOURNAL OF SYMBOLIC COMPUTATION[J]. 2017, 80: 62-86, http://dx.doi.org/10.1016/j.jsc.2016.07.010.
[70] Wang, Shuling, Nielson, Flemming, Nielson, Hanne Riis, Zhan, Naijun. Modelling and Verifying Communication Failure of Hybrid Systems in HCSP. COMPUTER JOURNAL[J]. 2017, 60(8): 1111-1130, http://dx.doi.org/10.1093/comjnl/bxw084.
[71] 詹乃军, 王戟, 李宣东. 软件形式化方法与应用专题前言. 软件学报[J]. 2016, 495-496, http://lib.cqvip.com/Qikan/Article/Detail?id=668151119.
[72] Gan Ting, Dai Liyun, Xia Bican, Zhan Naijun, Kapur Deepak, Chen Mingshuai, Olivetti N, Tiwari A. Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. AUTOMATED REASONING (IJCAR 2016)null. 2016, 9706: 195-212, [73] Yan Gaogao, Jiao Li, Li Yangjia, Wang Shuling, Zhan Naijun, Fitzgerald J, Heitmeyer C, Gnesi S, Philippou A. Approximate Bisimulation and Discretization of Hybrid CSP. FM 2016: FORMAL METHODSnull. 2016, 9995: 702-720, [74] 詹乃军. Barrier certificate revisited. Journal of Symbolic Computation. 2016, [75] Gan Ting, Chen Mingshuai, Li Yangjia, Xia Bican, Zhan Naijun, IEEE. Computing Reachable Sets of Linear Vector Fields Revisited. 2016 EUROPEAN CONTROL CONFERENCE (ECC)null. 2016, 419-426, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000392695300068.
[76] 詹乃军. Validated simulation-based verification of delayed differential dynamics. FM 2016. 2016, [77] Gan Ting, Chen Mingshuai, Dai Liyun, Xia Bican, Zhan Naijun, Finkbeiner B, Pu G, Zhang L. Decidability of the Reachability for a Family of Linear Vector Fields. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015null. 2015, 9364: 482-499, [78] 郭丹青, 吕继东, 王淑灵, 唐涛, 詹乃军, 周达天, 邹亮. 中国高速铁路列控系统的形式化分析与验证. 中国科学. 信息科学[J]. 2015, 45(3): 417-438, https://www.sciengine.com/doi/10.1360/N112014-00017.
[79] Ahmad Ehsan, Dong YunWei, Larson Brian, Lu JiDong, Tang Tao, Zhan NaiJun. Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2015, 58(11): https://www.sciengine.com/doi/10.1007/s11432-015-5346-2.
[80] Zou Liang, Zhan Naijun, Wang Shuling, Fraenzle Martin, Finkbeiner B, Pu G, Zhang L. Formal Verification of Simulink/Stateflow Diagrams. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015null. 2015, 9364: 464-481, [81] Ahmad Ehsan, Dong YunWei, Larson Brian, Lu JiDong, Tang Tao, Zhan NaiJun. Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2015, 58(11): http://dx.doi.org/10.1007/s11432-015-5346-2.
[82] Zou Liang, Fraenzle Martin, Zhan Naijun, Mosaad Peter Nazier, Kroening D, Pasareanu CS. Automatic Verification of Stability and Safety for Delay Differential Equations. COMPUTER AIDED VERIFICATION, CAV 2015, PT IInull. 2015, 9207: 338-355, [83] Liu Jiang, Zou Liang, Zhao Hengjun, Zhan Naijun. Abstraction of elementary hybrid systems by variable transformation. 20TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS, FM 2015null. 2015, 360-377, http://www.chinair.org.cn/handle/1471x/1660850.
[84] Liu Jiang, Zhan Naijun, Zhao Hengjun, Zou Liang, Bjorner N, DeBoer F. Abstraction of Elementary Hybrid Systems by Variable Transformation. FM 2015: FORMAL METHODSnull. 2015, 9109: 360-377, [85] Liu Jiang, Xu Ming, Zhan Naijun, Zhao Hengjun. Discovering non-terminating inputs for multi-path polynomial programs. JOURNAL OF SYSTEMS SCIENCE & COMPLEXITY[J]. 2014, 27(6): 1286-1304, https://www.webofscience.com/wos/woscc/full-record/WOS:000345627000013.
[86] Liu Jiang, Xu Ming, Zhan Naijun, Zhao Hengjun. Discovering non-terminating inputs for multi-path polynomial programs. JOURNAL OF SYSTEMS SCIENCE & COMPLEXITY[J]. 2014, 27(6): 1286-1304, https://www.webofscience.com/wos/woscc/full-record/WOS:000345627000013.
[87] 詹乃军. Adding Formal Meanings to AADL Models with Hybrid Annex. FACS 2014. 2014, [88] Dong Ruzhen, Zhan Naijun, Fiadeiro JL, Liu Z, Xue J. Towards a Failure Model of Software Components. FORMAL ASPECTS OF COMPONENT SOFTWAREnull. 2014, 8348: 119-136, [89] Guelev Dimitar P, Wang Shuling, Zhan Naijun, Zhou Chaochen. Super-dense computation in verification of hybrid CSP processes. 10th International Symposium on Formal Aspects of Component Software, FACS 2013null. 2014, 13-22, http://ir.iscas.ac.cn/handle/311060/16514.
[90] 詹乃军. An AADL Extension for Continuous Behavior and Cyber-Physical Interaction Modeling. HILT 2014. 2014, [91] Zhao Hengjun, Yang Mengfei, Zhan Naijun, Gu Bin, Zou Liang, Chen Yao, Jones C, Pihlajasaari P, Sun J. Formal Verification of a Descent Guidance Control Program of a Lunar Lander. FM 2014: FORMAL METHODSnull. 2014, 8442: 733-748, [92] Zhao Hengjun, Yang Mengfei, Zhan Naijun, Gu Bin, Zou Liang, Chen Yao. Formal verification of a descent guidance control program of a lunar lander. 19th International Symposium on Formal Methods, FM 2014null. 2014, 733-748, http://ir.iscas.ac.cn/handle/311060/16511.
[93] 詹乃军. 中国高速列车控制系统形式分析与验证. 中国科学. 2014, [94] 詹乃军. Generating nonlinear interpolants by semi-definite programming. CAV 2013. 2013, [95] Quan Zu, Miaomiao Zhang, Jiaqi Zhu, Naijun Zhan. Bounded model-checking of discrete duration calculus. HSCC 2013[J]. 2013, [96] 詹乃军. Super-dense computation in verification of HCSP processes. FACS 2013. 2013, [97] Zou, Liang, Zhan, Naijun, Wang, Shuling, Fraenzle, Martin, Qin, Shengchao, IEEE. Verifying Simulink Diagrams Via A Hybrid Hoare Logic Prover. 2013 PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE (EMSOFT)null. 2013, [98] Gao, Yang, Xu, Ming, Zhan, Naijun, Zhang, Lijun. Model checking conditional CSL for continuous-time Markov chains. INFORMATION PROCESSING LETTERS[J]. 2013, 113(1-2): 44-50, https://www.webofscience.com/wos/woscc/full-record/WOS:000312175200009.
[99] 詹乃军. Verifying Chinese Train Control Systems Under a Combined Scenario by Theorem Provig. VSTTE 2013. 2013, [100] Gao Yang, Hahn Ernst Moritz, Zhan Naijun, Zhang Lijun. CCMC: A conditional CSL model checker for continuous-time Markov chains. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013null. 2013, 464-468, http://ir.iscas.ac.cn/handle/311060/16659.
[101] 詹乃军. An interface model of software components. ICTAC 2013. 2013, [102] 詹乃军. Synthesizing switching controllers for hybrid systems by generating invariants. Festschrift of Jifeng He. 2013, [103] Zhao Hengjun, Zhan Naijun, Kapur Deepak, Larsen Kim G. A "hybrid" approach for synthesizing optimal controllers of hybrid systems: a case study of the oil pump industrial example. LECTURE NOTES IN COMPUTER SCIENCE (INCLUDING SUBSERIES LECTURE NOTES IN ARTIFICIAL INTELLIGENCE AND LECTURE NOTES IN BIOINFORMATICS)null. 2012, 471-485, http://ir.iscas.ac.cn/handle/311060/15770.
[104] Wang Shuling, Zhan Naijun, Guelev Dimitar. An assume/guarantee based compositional calculus for hybrid csp. LECTURE NOTES IN COMPUTER SCIENCE (INCLUDING SUBSERIES LECTURE NOTES IN ARTIFICIAL INTELLIGENCE AND LECTURE NOTES IN BIOINFORMATICS)null. 2012, 72-83, http://ir.iscas.ac.cn/handle/311060/15723.
[105] 詹乃军. Unblockable compositions of software components. CBSE 2012. 2012, [106] Xia, Bican, Yang, Lu, Zhan, Naijun, Zhang, Zhihai. Symbolic decision procedure for termination of linear programs. FORMAL ASPECTS OF COMPUTING[J]. 2011, 23(2): 171-190, https://www.webofscience.com/wos/woscc/full-record/WOS:000288029200003.
[107] Liu Jiang, Zhan Naijun, Zhao Hengjun. Computing semi-algebraic invariants for polynomial dynamical systems. EMBEDDED SYSTEMS WEEK 2011, ESWEEK 2011 - PROCEEDINGS OF THE 9TH ACM INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE, EMSOFT'11null. 2011, 97-106, http://ir.iscas.ac.cn/handle/311060/16221.
[108] 詹乃军. Refinement theories of software components. ACM SIGAPP SAC 2010, pp.2311-2318. 2010, [109] 詹乃军. A calculus for HCSP. A keynote of APLAS 2010, LNCS 6461, pp.1-15. 2010, [110] 詹乃军. Rate Monotonic Scheduling Re-analyzed. Information Processing Letters 110(6):226-231. 2010, [111] Xu, Qiwen, Zhan, Naijun. Rate monotonic scheduling re-analysed. INFORMATION PROCESSING LETTERS[J]. 2010, 110(6): 226-231, https://www.webofscience.com/wos/woscc/full-record/WOS:000275071900006.
[112] Yang, Lu, Zhou, Chaochen, Zhan, Naijun, Xia, Bican. Recent advances in program verification through computer algebra. FRONTIERS OF COMPUTER SCIENCE IN CHINA[J]. 2010, 4(1): 1-16, http://dx.doi.org/10.1007/s11704-009-0074-7.
[113] Zhan, Naijun. Connection between logical and algebraic approaches to concurrent systems. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE[J]. 2010, 20(5): 915-950, https://www.webofscience.com/wos/woscc/full-record/WOS:000284044600010.
[114] Zhan, Naijun, MajsterCederbaum, Mila. On hierarchically developing reactive systems. INFORMATION AND COMPUTATION[J]. 2010, 208(9): 997-1019, http://dx.doi.org/10.1016/j.ic.2010.04.002.
[115] Zhang, Miaomiao, Liu, Zhiming, Zhan, Naijun, Arbab, F, Sirjani, M. Model Checking Linear Duration Invariants of Networks of Automata. FUNDAMENTALS OF SOFTWARE ENGINEERINGnull. 2010, 5961: 244-+, [116] Chen, Zhenbang, Liu, Zhiming, Ravn, Anders P, Stolz, Volker, Zhan, Naijun. Refinement and verification in component-based model-driven design. SCIENCEOFCOMPUTERPROGRAMMING[J]. 2009, 74(4): 168-196, http://dx.doi.org/10.1016/j.scico.2008.08.003.
[117] Yang, Lu, Zhan, Naijun, Xia, Bican, Zhou, Chaochen, Meyer, B, Woodcock, J. Program verification by using DISCOVERER. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTSnull. 2008, 4171: 528-+, [118] 詹乃军. Refinement and composition of components in rCOS. In Proc. of UTP’08, Lecture Notes in Computer Science 5713, pp.238-257. 2008, [119] Zhang Jian, Zhang Wenhui, Zhan Naijun, Shen Yidong, Chen Haiming, Zhang Yunquan, Wang Yongji, Wu Enhua, Wang Hongan, Zhu Xueyang. Basic research in computer science and software engineering at sklcs. FRONTIERS OF COMPUTER SCIENCE IN CHINA[J]. 2008, 2(1): 1-11, [120] Xia Bican, Yang Lu, Zhan Naijun, Margaria T, Steffen B. Program Verification by Reduction to Semi-algebraic Systems Solving. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION, PROCEEDINGSnull. 2008, 17: 277-+, [121] 詹乃军. Modelling with Relational Calculus of Object and Component Systems – rCOS. In Proc. of CoCoME, Lecture Notes in Computer Science 5153, pp. 116-145. 2007, [122] Chen Yinghua, Xia Bican, Yang Lu, Zhan Naijun, Zhou Chaochen, Jones CB, Liu Z, Woodcock J. Discovering non-linear ranking functions by solving semi-algebraic systems. THEORETICAL ASPECTS OF COMPUTING - ICTAC 2007, PROCEEDINGSnull. 2007, 4711: 34-+, [123] 詹乃军. Reducing polynomial invariant generation to solving semi- algebraic systems. In Proc. of Formal Methods and Real-Time Systems, Lecture Notes in Computer Science 4700. 2007, [124] 詹乃军. 高阶时段演算及其完备性. 中国科学:E辑[J]. 2001, 31(1): 71-85, http://lib.cqvip.com/Qikan/Article/Detail?id=4997371.
[125] 詹乃军. 高阶时段演算及其完备性. 中国科学:E辑[J]. 2001, 31(1): 71-85, http://lib.cqvip.com/Qikan/Article/Detail?id=4997371.
[126] Guelev, Dimitar, Wang, Shuling, Zhan, Naijun. Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus. http://arxiv.org/abs/1706.06246.
[127] Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, JoostPieter Katoen. Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming. INFORMATION AND COMPUTATION. http://dx.doi.org/10.1016/j.ic.2022.104965.
[128] Peng, Yu, Wang, Shuling, Zhan, Naijun, Zhang, Lijun. Extending Hybrid CSP with Probability and Stochasticity. http://arxiv.org/abs/1509.01660.
[129] Liu, Jiang, Zhan, Naijun, Zhao, Hengjun. Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems. http://arxiv.org/abs/1103.3372.
发表著作
(1) 混成系统的形式建模、分析与验证, Formal Modelling, Analysis, Verification of Hybrid Systems, Springer-Verlag, 2013-05, 第 1 作者
(2) Combining Formal and Informal Methods in the Design of Spacecrafts, Springer, 2016-01, 第 2 作者
(3) 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., Springer, 2016-10, 第 3 作者
(4) Formal Verification of Simulink/Stateflow Diagrams: A Deductive Way, Springer, 2016-12, 第 1 作者
(5) 形式语义学引论, 科学出版社, 2017-10, 第 2 作者
(6) 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., Springer, 2018-04, 第 3 作者
(7) Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2019, ACM, 2019-10, 第 4 作者

科研活动

       中国计算机学会形式化方法专委会副主任 

       Editorial Boards of  Formal Aspects of ComputingJournal of Logical and Algebraic Methods in ProgrammingJournal of Softwareand Computer Research and Development

       Steering committee members of MEMOCODESETTA

       PC members of

       2021: FM (co-chair), HSCC, ADHS, EMSOFT, TASE

       2020: CAV, RTSS, HSCC, EMSOFT, TTSS, TASE, ICFEM, iFM, SNR

       2019: RTSS, EMSOFT, ICFEM, TASE, TAMC, ICESS (general co-chair), iFM, UTP, MEMOCODE (general co-chair)

       2018: QEST, SNR, ADHS, ATVA, MEMOCODE (general co-chair), FMAC

       2017: TAMC, SETTA, ICTAC, ICECCS, FMAC

       2016: HSCC, UTPSETTA (PC co-chair), ICTAC, VSTTEATVA, FACS

       2015: HSCC, ATVA, TASE, ICECCS, WPHS

       2014: HSCC, TAMC, ICTAC, UTP, FACS, TASE, ICECCSEASLLC, FSFMA, HTSS

       2013: ICTAC, ICECCS, HTSS, FACS, FSFMA, RIVF, COMPUTATION TOOLS

       2012: ICECCS, ICTAC, RIVF, TIMES, TAMC, TASE, UTP, COMPUTATION TOOLS

       2011: KSE, ICFEM, TIMES, COMPUTATION TOOLS

       2010: ICTAC, KSE, FACS, UTP

       2009: ICTAC, KSE, FACS

       2008: ICTAC, HTSS

       2007: ICTAC, HTSS

       2006: ICECCS


在研项目
( 1 ) 航天嵌入式软件可信性保障集成环境 和示范验证与应用, 主持, 国家级, 2012-01--2016-12
( 2 ) 安全攸关软件系统的构造与质量保障方法研究, 参与, 国家级, 2014-01--2018-12
( 3 ) 航天嵌入式软件设计一致性验证技术及其应用, 主持, 国家级, 2015-01--2016-12
( 4 ) 安全攸关软件理论和质量保障方法创新国际团队, 主持, 部委级, 2014-01--2018-12
( 5 ) 复杂安全攸关嵌入式系统形式设计, 主持, 国家级, 2017-01--2021-12
( 6 ) 面向程序验证的自动定理证明理论、方法和工具研究, 参与, 国家级, 2018-01--2022-12
( 7 ) 智能控制系统形式设计验证及应用, 主持, 国家级, 2019-06--2022-05
参与会议
(1)• Invariant Generation by Constraint Solving in Verification of Programs and Hybrid   2020-12-11
(2)• Taming Delays in Cyber-Physical Systems   2020-12-03
(3)• Taming Delays in Cyber-Physical Systems   2020-12-01
(4)• Non-linear interpolant generation and its application to program verification   2020-09-04
(5)• Practical Verification of Intelligent CPSs   2020-07-03
(6) Formal Analysis, Verification and Design of Safety-Critical CPS   2019-12-03
(7)Taming Delays in Cyber-Physical Systems   2019-11-08
(8) Generating SystemC code from delay HCSP   2017-11-27
(9) Generating SystemC code from HCSP Formal Models   2017-11-03
(10)Formal Design of Embedded Systems   西湖论坛   2017-10-28
(11)Formal Design of Embedded Systems   中国数学学会数理逻辑专业委员会年会   2017-05-27

指导学生

已指导学生

权曌  硕士研究生  430112-计算机技术  

赵恒军  博士研究生  081202-计算机软件与理论  

高杨  硕士研究生  081202-计算机软件与理论  

邹亮  博士研究生  081202-计算机软件与理论  

郭丹青  硕士研究生  081202-计算机软件与理论  

彭宇  硕士研究生  081202-计算机软件与理论  

陈明帅  博士研究生  081202-计算机软件与理论  

刘涛  硕士研究生  081202-计算机软件与理论  

王健  硕士研究生  081202-计算机软件与理论  

占浩澜  硕士研究生  081202-计算机软件与理论  

林倩倩  硕士研究生  081202-计算机软件与理论  

现指导学生

王秋野  博士研究生  081202-计算机软件与理论  

王令泰  博士研究生  081202-计算机软件与理论  

冯胜华  博士研究生  081202-计算机软件与理论  

杨腾舜  博士研究生  081202-计算机软件与理论  

苏涵  博士研究生  081202-计算机软件与理论  

吴昊  硕士研究生  081200-计算机科学与技术  

金翔宇  博士研究生  083500-软件工程