基本信息
詹乃军男博导中国科学院软件研究所
电子邮件： znj@ios.ac.cn
通信地址： 北京中关村南四街4号，8718信箱
邮政编码： 100190
部门/实验室：计算机科学国家重点实验室
研究领域实时和混成系统、信息物理融合系统、形式化方法、计算语义模型、程序验证

招生信息博士一名，硕士一名
招生专业081202-计算机软件与理论

招生方向信息物理融合系统CPS
程序理论与验证技术
基于构件的开发方法


教育背景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）Probably Approximate Safety Verification of Hybrid Dynamical Systems,In Proc. of ICFEM 2019, Lecture Notes in Computer Science 11852,2019-11,第4作者
（2）Automatically generating SystemC code from HCSP formal mdoels,ACM Transaction on Software Engineering and Methodoloty,2019-10,通讯作者
（3）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-10,通讯作者
（4）In decision and delays are the parents of failure -- Taming them algorithmically by synthesizing delay-resilient control,Acta Informatica,2019,通讯作者
（5）Inner approximating reachable sets for polynomial systems with time-varying uncertainties,IEEE Transaction on Automatic Control,2019,第3作者
（6）Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations,CAV 2019,2019,通讯作者
（7）Formal verification of quantum algorithms using quantum Hoare logic,CAV 2019,2019,第8作者
（8）NIL: Learning Nonlinear Interpolants,CADE 2019,2019,通讯作者
（9）Robust Invariant Sets Generation for State-Constrained Perturbed Polynomial Systems,HSCC 2019,2019,第4作者
（10）Model Checking Continuous-time Bounded Extended Linear Duration Invariants,HSCC 2018,2018,通讯作者
（11）Under-Approximating Reach Sets for Polynomial Continuous Systems,HSCC 2018,2018,第3作者
（12）Monitoring CTMCs by multi-clock timed automata,CAV 2018,2018,通讯作者
（13）The opacity of real-time automata,IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems,2018,通讯作者
（14）Reachability analysis for solvable dynamical systems,IEEE Transaction on Automatic Control,2018,通讯作者
（15）What’s to come is still unsure: Synthesizing synthesizers resilient to delayed reaction,ATVA 2018,2018,通讯作者
（16）Reachability analysis for solvable dynamical systems,IEEE Transaction on Automatic Control,2018,通讯作者
（17）Generating semi-algebraic invariants for non-autonomous hybrid systems,Journal of System Science and Complexity,2017,通讯作者
（18）A compositional modelling and verification framework for stochastic hybrid systems,Formal Aspects of Computing,2017,通讯作者
（19）Modelling and Verifying Communication Failure of Hybrid Systems in HCSP,Computer Journal,2017,第4作者
（20）Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations,FORMATS,2017,第6作者
（21）Finding Polynomial Loop Invariants for Probabilistic Programs,ATVA 2017,2017,第4作者
（22）Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus,SETTA 2017, LNCS 10606,2017,第3作者
（23）Generating SystemC code from delay HCSP,APLAS 2017, LNCS 10695,2017,通讯作者
（24）Approximate bisimulation and discretization of Hybrid CSP,FM 2016,2016,通讯作者
（25）Validated simulation-based verification of delayed differential dynamics,FM 2016,2016,通讯作者
（26）Computing reachable sets of linear vector fields revisited,ECC 2016,2016,通讯作者
（27）Interpolant synthesis for quadratic polynomial inequalities and combination with EUF,IJCAR 2016,2016,通讯作者
（28）Barrier certificate revisited,Journal of Symbolic Computation,2016,通讯作者
（29）Extending Hybrid CSP with Probability and Stochasticity,SETTA 2015,2015,通讯作者
（30）Decidability of the reachability for a family of linear vector fields,ATVA 2015,2015,通讯作者
（31）Formal verification of Simulink/Stateflow diagrams,ATVA 2015,2015,通讯作者
（32）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,2015,通讯作者
（33）Automatic stability and safety verification for delay differential equations,CAV 2015,2015,通讯作者
（34）Abstraction of elementary hybrid systems by variable transformation,FM 2015,2015,通讯作者
（35）Discovering non-terminating inputs for polynomial programs,Journal of System Science and Complexity 27(6),2014,通讯作者
（36）Formal verification of Simulink/Stateflow diagrams,ESWEEK 2014 (tutorial),2014,第1作者
（37）An AADL Extension for Continuous Behavior and Cyber-Physical Interaction Modeling,HILT 2014,2014,通讯作者
（38）Adding Formal Meanings to AADL Models with Hybrid Annex,FACS 2014,2014,通讯作者
（39）Formal verification of a descent guidance control program of a lunar lander,FM 2014,2014,通讯作者
（40）中国高速列车控制系统形式分析与验证,中国科学,2014,通讯作者
（41）Super-dense computation in verification of HCSP processes,FACS 2013,2013,第3作者
（42）Verifying Simulink diagrams via a Hybrid Hoare Logic prover,EMSOFT 2013,2013,通讯作者
（43）Bounded model-checking of discrete duration calculus,HSCC 2013,2013,通讯作者
（44）Model checking conditional CSL for continuous-time Markov chains,Inf. Process. Lett. 113(1-2): 44-50 ,2013,第3作者
（45）Generating nonlinear interpolants by semi-definite programming,CAV 2013,2013,通讯作者
（46）An interface model of software components,ICTAC 2013,2013,第2作者
（47）Synthesizing switching controllers for hybrid systems by generating invariants,Festschrift of Jifeng He,2013,通讯作者
（48）Verifying Chinese Train Control Systems Under a Combined Scenario by Theorem Provig,VSTTE 2013,2013,通讯作者
（49）Towards a failure model of software components,FACS 2013,2013,通讯作者
（50）A Hybrid Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example,FM 2012,2012,通讯作者
（51）Unblockable compositions of software components,CBSE 2012,2012,第2作者
（52）An Assume/Guarantee Based Compositional Calculus for Hybrid CSP,TAMC 2012,2012,通讯作者
（53）Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems,Mathematics in Computer Science 6(4): 395-408 ,2012,通讯作者
（54）Symbolic decision procedure for termination of linear programs,Formal Aspects of Computing ，23(2):171-190,2011,第3作者
（55）Computing semi-algebraic invariants for polynomial dynamical systems,EMSOFT 2011,2011,通讯作者
（56）Connection between logical and algebraic approaches to concurrent systems,Math. Struct. in Comp. Science 20:915-950,2010,第1作者
（57）On hierarchically developing reactive systems,Inf. Comput. 208(9): 997-1019,2010,第1作者
（58）Rate Monotonic Scheduling Re-analyzed,Information Processing Letters 110(6):226-231,2010,通讯作者
（59）A calculus for HCSP,A keynote of APLAS 2010, LNCS 6461, pp.1-15,2010,通讯作者
（60）Refinement theories of software components,ACM SIGAPP SAC 2010, pp.2311-2318,2010,通讯作者
（61）Advances in program verification through computer algebra,Frontiers of Computer Science in China 4(1):1-16,2010,通讯作者
（62）Model checking linear duration invariants of networks of automata,In Proc. FSEN’09, Lecture Notes in Computer Science 5961. pp.244-259,2009,通讯作者
（63）Refinement and verification in component based and model driven design,Science of Computer Programming 74(4):168-196,2009,通讯作者
（64）Refinement and composition of components in rCOS, In Proc. of UTP’08, Lecture Notes in Computer Science 5713, pp.238-257,2008,第1作者
（65）Program verification by reduction to semi-algebraic systems solving,in Proc. of ISoLA’08, CCIS-17,2008,通讯作者
（66）Modelling with Relational Calculus of Object and Component Systems – rCOS,In Proc. of CoCoME, Lecture Notes in Computer Science 5153, pp. 116-145,2007,通讯作者
（67）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,通讯作者
（68）Discovering non-linear ranking functions by solving semi- algebraic systems,In Proc. of ICTAC’07, Lecture Notes in Computer Science 4711,2007,通讯作者
（69）
（70）
（71）

发表著作（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作者


科研活动学术组织：ACM会员，欧洲计算机科学逻辑学会会员，欧洲符号逻辑学会会员，中国计算机学会高级会员;`
学术任职：ATVA2006的组织委员会主席,ICECCS2006, ICECCS2012, ICTAC2007, ICTAC2008, ICTAC2009, ICTAC2010, ICTAC2012, HTSS2007, HTSS2008, KSE2009, KSE2010, KSE2011, RIVF2012, FACS2009, FACS2010, ICFEM2011, TIMES2011, TIMES2012, COMPUTATION TOOLS 2011, COMPUTATION TOOLS 2012, TAMC2012, UTP2010, UTP2012, TASE2012 等国际会议的程序委员会委员。

在研项目（ 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） Formal Analysis, Verification and Design of Safety-Critical CPS2019-12-03
（2）Taming Delays in Cyber-Physical Systems2019-11-08
（3） Generating SystemC code from delay HCSP2017-11-27
（4） Generating SystemC code from HCSP Formal Models2017-11-03
（5）Formal Design of Embedded Systems西湖论坛2017-10-28
（6）Formal Design of Embedded Systems中国数学学会数理逻辑专业委员会年会2017-05-27


合作情况
项目协作单位

指导学生已指导学生
权曌硕士研究生430112-计算机技术
赵恒军博士研究生081202-计算机软件与理论
高杨硕士研究生081202-计算机软件与理论
邹亮博士研究生081202-计算机软件与理论
郭丹青硕士研究生081202-计算机软件与理论
彭宇硕士研究生081202-计算机软件与理论
陈明帅博士研究生081202-计算机软件与理论
刘涛硕士研究生081202-计算机软件与理论
王健硕士研究生081202-计算机软件与理论
现指导学生
王秋野博士研究生081202-计算机软件与理论
占浩澜硕士研究生081202-计算机软件与理论
林倩倩硕士研究生081202-计算机软件与理论
王令泰博士研究生081202-计算机软件与理论
冯胜华博士研究生081202-计算机软件与理论
金翔宇硕士研究生081202-计算机软件与理论
杨腾舜博士研究生081202-计算机软件与理论
苏涵博士研究生081202-计算机软件与理论