詹乃軍

詹乃軍，男，中國科學院大學教授。

基本介紹

• 中文名：詹乃軍
• 學位/學歷：博士
• 性別：男
• 職稱：教授

人物經歷

教育背景

1997-09--2000-07 中科院軟體所 博士

1993-09--1996-06 南京大學計算機科學與技術系 碩士

1989-09--1993-06 南京大學數學系 學士

工作經歷

2016-01~現在, 中國科學院, 特聘研究員

2015-03~現在, 中國科學院大學, 崗位教授

2008-10~現在, 中科院軟體所, 研究員

2004-09~2008-09,中科院軟體所, 副研究員

2001-05~2004-07,德國曼海姆大學, 助理研究員

出國學習

•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: 聯合國大學國際軟體技術研究所，做博士論文；

研究方向

實時和混成系統、信息物理融合系統、形式化方法、計算語義模型、程式驗證。

教授課程

本科生畢業設計（計算機科學與技術）

離散數學

數理邏輯與程式理論

模態和時序邏輯

混成系統建模和驗證

主要成就

發表論文

（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, 通訊作者

發表著作

（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 作者

獲獎記錄

（1） 航天嵌入式軟體可信保障關鍵技術和套用, 一等獎, 省級, 2019

（2） 實時和嵌入式系統形式設計理論, 三等獎, 省級, 2018

社會任職

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-今,《計算機研究與發展》編委。