詹乃军 男 博导 软件研究所
电子邮件: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: 联合国大学国际软件技术研究所,做博士论文;

工作经历

   
工作简历
2008-10--今 中科院软件所 研究员
2004-09--2008-09 中科院软件所 副研究员
2001-05--2004-07 德国曼海姆大学 助理研究员
社会兼职
2015-03--今 《Formal Aspects of Computing》编委
2015-01--今 FME Awards Committee
2015-01--今 《软件学报》编委
2014-03--今 《计算机研究与发展》编委

教授课程

模态和时序逻辑、 混成系统建模和验证

专利与奖励

   
奖励信息
   
专利成果
   

出版信息

   
发表论文
(1) Barrier certificate revisited,Journal of Symbolic Computation,2016,通讯作者
(2) Automatic stability and safety verification for delay differential equations,CAV 2015,2015,通讯作者
(3) Abstraction of elementary hybrid systems by variable transformation,FM 2015,2015,通讯作者
(4) 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,通讯作者
(5) Adding Formal Meanings to AADL Models with Hybrid Annex,FACS 2014,2014,通讯作者
(6) Discovering non-terminating inputs for polynomial programs,Journal of System Science and Complexity 27(6),2014,通讯作者
(7) Formal verification of a descent guidance control program of a lunar lander,FM 2014,2014,通讯作者
(8) 中国高速列车控制系统形式分析与验证,中国科学,2014,通讯作者
(9) An AADL Extension for Continuous Behavior and Cyber-Physical Interaction Modeling,HILT 2014,2014,通讯作者
(10) Formal verification of Simulink/Stateflow diagrams,ESWEEK 2014 (tutorial),2014,第1作者
(11) Synthesizing switching controllers for hybrid systems by generating invariants,Festschrift of Jifeng He,2013,通讯作者
(12) Generating nonlinear interpolants by semi-definite programming,CAV 2013,2013,通讯作者
(13) Verifying Simulink diagrams via a Hybrid Hoare Logic prover,EMSOFT 2013,2013,通讯作者
(14) Towards a failure model of software components,FACS 2013,2013,通讯作者
(15) An interface model of software components,ICTAC 2013,2013,第2作者
(16) Super-dense computation in verification of HCSP processes,FACS 2013,2013,第3作者
(17) Bounded model-checking of discrete duration calculus,HSCC 2013,2013,通讯作者
(18) Verifying Chinese Train Control Systems Under a Combined Scenario by Theorem Provig,VSTTE 2013,2013,通讯作者
(19) Model checking conditional CSL for continuous-time Markov chains,Inf. Process. Lett. 113(1-2): 44-50 ,2013,第3作者
(20) A Hybrid Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example,FM 2012,2012,通讯作者
(21) Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems,Mathematics in Computer Science 6(4): 395-408 ,2012,通讯作者
(22) An Assume/Guarantee Based Compositional Calculus for Hybrid CSP,TAMC 2012,2012,通讯作者
(23) Unblockable compositions of software components,CBSE 2012,2012,第2作者
(24) Computing semi-algebraic invariants for polynomial dynamical systems,EMSOFT 2011,2011,通讯作者
(25) Symbolic decision procedure for termination of linear programs,Formal Aspects of Computing ,23(2):171-190,2011,第3作者
(26) Refinement theories of software components,ACM SIGAPP SAC 2010, pp.2311-2318,2010,通讯作者
(27) Connection between logical and algebraic approaches to concurrent systems,Math. Struct. in Comp. Science 20:915-950,2010,第1作者
(28) On hierarchically developing reactive systems,Inf. Comput. 208(9): 997-1019,2010,第1作者
(29) Rate Monotonic Scheduling Re-analyzed,Information Processing Letters 110(6):226-231,2010,通讯作者
(30) A calculus for HCSP,A keynote of APLAS 2010, LNCS 6461, pp.1-15,2010,通讯作者
(31) Advances in program verification through computer algebra,Frontiers of Computer Science in China 4(1):1-16,2010,通讯作者
(32) Refinement and verification in component based and model driven design,Science of Computer Programming 74(4):168-196,2009,第5作者
(33) Model checking linear duration invariants of networks of automata,In Proc. FSEN’09, Lecture Notes in Computer Science 5961. pp.244-259,2009,通讯作者
(34) Program verification by reduction to semi-algebraic systems solving,in Proc. of ISoLA’08, CCIS-17,2008,通讯作者
(35) Refinement and composition of components in rCOS, In Proc. of UTP’08, Lecture Notes in Computer Science 5713, pp.238-257,2008,第1作者
(36) Discovering non-linear ranking functions by solving semi- algebraic systems,In Proc. of ICTAC’07, Lecture Notes in Computer Science 4711,2007,通讯作者
(37) Modelling with Relational Calculus of Object and Component Systems – rCOS,In Proc. of CoCoME, Lecture Notes in Computer Science 5153, pp. 116-145,2007,通讯作者
(38) 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,通讯作者
发表著作
(1) 混成系统的形式建模、分析与验证,Formal Modelling, Analysis, Verification of Hybrid Systems,Springer-Verlag,2013-05,第1作者

科研活动

学术组织: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) 航天嵌入式软件设计一致性验证技术及其应用,主持,国家级,2015-01--2016-12
(2) 安全攸关软件理论和质量保障方法创新国际团队,主持,院级级,2014-01--2018-12
(3) 安全攸关软件系统的构造与质量保障方法研究,参与,国家级,2014-01--2018-12
(4) 航天嵌入式软件可信性保障集成环境 和示范验证与应用,参与,国家级,2012-01--2016-12
参与会议
   

合作情况

   
项目协作单位
   

指导学生

已指导学生

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

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

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

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

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

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

现指导学生

李勇  硕士研究生  081202-计算机软件与理论  

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

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

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