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