北京航空航天大學

導師詳細信息

姓名：佘志坤

性別：男

出生年份：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) 佘志坤，劉鐵鋼，鄭志明�？臻g非開普勒軌道分析與控制中的數學問題。宇航學報。第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.