北京航空航天大学数学与系统科学学院应用数学导师介绍：佘志坤

导师详细信息

姓名：佘志坤

性别：男

出生年份：1977

职称：教授

院系：数学与系统科学学院

首次聘任导师时间：2009

现聘任导师一级学科名称：数学

现聘任导师二级学科名称：应用数学

聘任在第二学科培养博士生专业名称：无

聘任在自主设置学科培养博士生专业名称：无

主要研究方向及特色：研究方向：混成系统自动验证、微分方程与动力系统、符号－数值计算、计算复杂性、空间非开普勒轨道分析与控制；研究特色：属于交叉领域的基础及应用研究，涉及到数学、计算机科学和系统科学。欢迎有兴趣的硕士生、博士生与博士后加盟其中。

电子信箱：zhikun.she@buaa.edu.cn

办公电话：82317930

办公地点：图书馆西配楼518房间

通信地址：北京市海淀区学院路37号院

个人简介：

个人情况简介:

佘志坤，男，1977年出生。北京航空航天大学数学与系统科学学院教授、博士生导师。2007年度北京市优秀人才，2007年度北京航空航天大学蓝天新秀，2008年度北京市科技新星，2013年度教育部新世纪优秀人才，2014年度国家优秀青年科学基金项目获得者。获2013年度教育部自然科学奖一等奖（第三完成人）。1995年9月到2005年6月，就读于北京大学数学科学学院，获理学学士和博士学位（硕博连读）；2004年1月到2006年12月，工作于德国马普计算机科学研究所。

他主要在混成系统自动验证、微分方程和动力系统、符号-数值计算、计算复杂性、空间非开普勒轨道分析与优化控制等领域从事基础和应用研究。博士期间，在导师郑志明教授的指导下，提出了伪除机理论，从而推广了Smale等提出的著名的BSS机器(即所谓的实图灵机模型)，并在2002年国际数学家大会分会场做此研究成果的报告。以此为基础，在实代数系统的研究上也取得了一系列原创成果。Herbrand奖得主、德国马普计算机科学研究所前所长H.Ganzinger教授高度重视，特意邀请他前往德国马普计算机科学研究所做短期访问；随后，在未取得博士学位情况下，他被破格邀请到马普从事博士后研究，并进入德国大型跨区域科研项目AVACS（www.avacs.org）的核心研究小组之中。

在混成系统自动验证领域，他对非线性混成系统安全性自动验证问题进行了直接处理，突破了之前理论主要通过线性近似来讨论的局限性，并开发了自动验证软件Hsolver（hsolver.sourceforge.net/）。由美国工程院院士Alberto L. Sangiovanni-Vincentelli发表的、详细介绍国际上混成系统研究方面最新进展的综述性学术论文《Languages and Tools for Hybrid Systems Design》（Foundations and Trends in Electronic Design Automation. Vol. 1, No 1/2 (2006), 1-193）在134至140页介绍的就是其工作，其评价是“HSolver improves the traditional method by implementing a pruning algorithm that removes uninteresting parts of the state space before reducing the grid size. Consequently, the refinement of the over-approximation can be obtained even without increasing the number of grid locations, one of the causes of exponential blowout in the verification algorithms for hybrid systems”、“The language for describing hybrid systems is very easy to understand. There are no limitations in describing a single automaton and the limited number of statements in the language makes it simple to use”。
归国后，他把混杂(成)系统引入到空间非开普勒轨道的分析与优化控制之中，被誉为“从混杂系统研究空间轨道构思新颖，是航天器轨道研究的一个新方向”。发表在《宇航学报》的学术论文《空间非开普勒轨道分析与控制中的数学问题》被西北工业大学精品课程《航天器飞行力学》列为学科前沿（http://jpkc.nwpu.edu.cn/jp2011/04/xuekeqianyan.html）。

他独立撰写国防报告3部，在ACM Transactions on Embedded Computing Systems、SIAM Journal on Control and Optimization、Journal of Symbolic Computation、Celestial Mechanics and Dynamical Astronomy等领域国际顶级刊物和AAAI、CAV、ISSAC、HSCC等领域国际顶级会议上发表学术论文40余篇。研究成果被来自于Massachusetts Institute of Technology、Stanford University、University of California at Berkeley、University of Cambridge、University of Oxford、ETH Zurich、Carnegie Mellon University、RWTH Aachen、日本早稻田大学、新加坡国立大学、清华大学、CNRS、INRIA、MPII、中国科学院软件所等国内外著名机构的学者他引300余次，单篇最高他引90余次。特别地，图灵奖得主Edmund M. Clarke、美国工程院院士Alberto L. Sangiovanni-Vincentelli、美国工程院院士、欧洲科学院院士Moshe Y. Vardi、欧洲科学院院士Marta Kwiatkowska、清华大学孙家广院士、斯坦福大学Prof. Zohre Manna、ACM会士、IEEE会士Prof. John A. Stankovic、ACM会士Prof. Lawrence Paulson、IEEE会士Prof. Bruce Krogh、IEEE会士Prof. Bud Mishra、IEEE会士Prof. Insup Lee、IEEE会士Prof. John Lygeros、IEEE会士Prof. George Pappas等给予了积极的正面评价，诸如“明显优势”、“极大改进”、“灵感之源”等等。

自2007年以来承担科研项目情况：

1）参与973项目“海量信息的协同性和可生存性的理论与实践研究”的“海量信息系统协同性和可生存性的随机模型研究”课题组(2005CB321902，2006-2010)。

2）主持2007年度北京市优秀人才资助项目“混杂系统自动验证和分析”(2007.01-2008.12)；

3）主持教育部留学归国人员科研启动基金“混杂系统自动验证与分析”(2008.01-2009.12)；

4）主持国家军口863项目“XXXXXXXXXXXXXXXX关键技术研究”(2008.07-2010.06，70万)；

5）主持2008年度北京市科技新星计划项目“混杂系统自动验证及其在软件可靠性中的应用”(2009.01-2011.12，25万)；

6）主持国家军口863项目“XXXXXXXXXXXXXX可靠性研究”(2010.07-2011.06，30万)；

7）主持国家自然基金项目“基于代数分析与符号计算的混成系统自动验证”（2011.01-2013.12，20万）；

8）主持软件开发环境国家重点实验室自选课题“基于微分不变量的混成系统安全性自动验证”（2011.05-2013.05,15万）；

9）主持北航领航基金“海量信息知识体系发现与进化中的关键问题研究”(2011.01-2011.12,10万)。

任现职以来发表的代表性论文：

19) L. Zhang, Z. She, S. Ratschan, H. Hermanns, E. M. Hahn. Safety Verification for Probabilistic Hybrid Systems. accepted for European Journal of Control, 2011.

18) Zhikun She and Bai Xue. Computing a basin of attraction to a target region by solving bilinear semi-definite problems. In Proceedings of the 13th International Workshop in Computer Algebra in Scientific Computing, Lecture Notes in Computer Science, Vol. 6885, pp. 333-344, Springer, 2011.

17) Zhikun She. Termination Analysis of Safety Verification for Non-linear Robust Hybrid Systems. In Proceedings of the 8th International Conference on Informatics in Control, Automation and Robotics, pp. 251-261, SciTePress, 2011. (full paper, 接受率10%, 共322份投稿)

16) Zhikun She, Bai Xue and Zhiming Zheng. Algebraic Analysis on Asymptotic Stability of Continuous Dynamical Systems. In Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, pp. 313-320, 2011. (ISSAC为计算机科学“Algorithms and Theory”的顶级会议)

15) Zhikun She, Bican Xia and Zhiming Zheng. Condition number based complexity estimate for solving polynomial systems. Journal of Computational and Applied Mathematics, 235(8): 2670-2678, Elsevier, 2011.

14) Zhikun She, Jing Yu and Bai Xue. Controllable Laws for Stability Analysis of Switched Linear Systems. In Proceedings of the 3rd IEEE International Conference on Computer and Network Technology, Vol. 13, pp. 127-131, 2011.

13) Stefan Ratschan and Zhikun She. Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-like Functions. SIAM Journal on Control and Optimization, 48(7): 4377-4394, 2010.

12) Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst M. Hahn. Safety Verification for Probabilistic Hybrid Systems. In Proceedings of the 22nd International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 6174, pp. 196-211, Springer, 2010. (CAV为计算机科学“Programming Languages and Software Engineering”的顶级会议)（Scholar google 搜索结果，9次引用）

11) 薛白，佘志坤，余婧，刘铁钢，郑志明。基于混杂系统的空间飞行器悬停控制。中国空间科学技术。第30卷，第2期，pp. 61-67, 2010.

10) H. Zhou, Q. Cheng and Z. She. Reparameterization based consistent graph-structured linear programs. In Proceedings of the 25th ACM Symposium on Applied Computing, pp. 974-978, 2010.

9) 佘志坤，薛白，丛源良，刘铁钢，郑志明。最优双冲量交会问题的数学建模与数值求解。宇航学报。第31卷，第1期，pp. 155-161, 2010.

8) 裴森，孙野，赵珍，王海涛，余志坤. 一类一维混沌映射的拓扑条件。第39卷，第19期，pp. 213-227, 2009.

7) Zhikun She, Ranran Yan, Bai Xue and Zhiming Zheng. On the Algebraization of Asymptotic Stability Analysis for Differential Systems. In Proceedings of the 11th IASTED International Conference on Control and Applications, pp. 68-74, ACTA Press, 2009.

6) Zhikun She and Zhiming Zheng. Condition number based complexity estimate for solving local extrema. Journal of Computational and Applied Mathematics, 230(1), pp. 233-242, Elsevier, 2009.

5) Zhikun She, Bican Xia, Rong Xiao and Zhiming Zheng. A semi-algebraic approach for asymptotic stability analysis. Nonlinear Analysis: Hybrid Systems, 3(4), 588-596, Elsevier, 2009.

4) 佘志坤，刘铁钢，郑志明。空间非开普勒轨道分析与控制中的数学问题。宇航学报。第30卷，第1期，pp. 54-58, 2009.

3) Zhikun She and Zhiming Zheng. Tightened Reachability Constraints for the Verification of Linear Hybrid Systems. Nonlinear Analysis: Hybrid Systems, Vol. 2, No. 4, pp. 1222-1231, Elsevier, 2008.

2) Stefan Ratschan and Zhikun She. Recursive and Backward Reasoning in the Verification of Hybrid Systems. In Proceedings of the Fifth International Conference on Informatics in Control, Automation and Robotics, Vol. 4, pp. 65-71, SciTePress, 2008.

1) Zhikun She and Zhiming Zheng. Tightened reachability constraints for safety verification of linear hybrid systems. In Proceedings of the 10th IASTED International Conference on Intelligent Systems and Control, pp. 383-388, ACTA Press, 2007.

任现职之前的代表性论文（与博士后合作导师S. Ratschan合作的文章全按字母排序，可参看S. Ratschan主页里的说明）：

7) S. Ratschan and Z. She. Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Transactions on Embedded Computing Systems, Vol. 6, No. 1, Article No. 8, pp. 1-23, 2007. （Scholar google 搜索结果，44次引用）

6) F. Klaedtke, S. Ratschan, and Z. She. Language-based abstraction refinement for hybrid system verification. In Verification, Model Checking and Abstraction Interpretation. Lecture Notes in Computer Science, Vol. 4349, pp. 151-166, Springer, 2007.

5) Zhikun She, Bican Xia and Rong Xiao. A Semi-Algebraic Approach for the Computation of Lyapunov Functions. In Proceedings of the 2nd IASTED International Conference on Computational Intelligence, pp. 7-12, ACTA Press, 2006.

4) Stefan Ratschan and Zhikun She. Providing a Basin of Attraction to a Target Region by Computation of Lyapunov-like Functions. In Bela Patkai and Imre J. Rudas (Eds.): Proceedings of the 4th IEEE International Conference on Computational Cybernetics, pp. 245-249, 2006.

3) Stefan Ratschan and Zhikun She. Constraints for Continuous Reachability in the Verification of Hybrid Systems. In Jacques Calmet, Tetsuo Ida and Dongming Wang (Eds.): AISC 2006, Lecture Notes in Computer Science, Vol. 4120, pp. 196-210, Springer-Verlag, 2006. （Scholar google 搜索结果，11次引用）

2) S. Ratschan and Z. She. Safety Verification of Hybrid System by Constraint Propagation Based Abstraction Refinement. In M. Morari and L. Thiele (Eds.): HSCC 2005, Lecture Notes in Computer Science, Vol. 3414, pp. 573-589, Springer-Verlag, 2005. （Scholar google 搜索结果，59次引用）

1) She Zhikun, Xia Bican and Zheng Zhiming. Pseudo-Division Machine(I): A Model of Symbolic Computation. In Proceedings of the 1st International Congress of Mathematical Software: Mathematical Software, pp. 115-125, World Scientific, Singapore, 2002.