北京航空航天大學(xué)

主要研究方向及特色：研究方向：混成系統(tǒng)自動驗證、微分方程與動力系統(tǒng)、符號－數(shù)值計算、計算復(fù)雜性、空間非開普勒軌道分析與控制；研究特色：屬于交叉領(lǐng)域的基礎(chǔ)及應(yīng)用研究，涉及到數(shù)學(xué)、計算機科學(xué)和系統(tǒng)科學(xué)。歡迎有興趣的碩士生、博士生與博士后加盟其中。

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

辦公電話：82317930

辦公地點：圖書館西配樓518房間

通信地址：北京市海淀區(qū)學(xué)院路37號院

個人簡介：

個人情況簡介:

佘志坤，男，1977年出生。北京航空航天大學(xué)數(shù)學(xué)與系統(tǒng)科學(xué)學(xué)院教授、博士生導(dǎo)師。2007年度北京市優(yōu)秀人才，2007年度北京航空航天大學(xué)藍(lán)天新秀，2008年度北京市科技新星，2013年度教育部新世紀(jì)優(yōu)秀人才，2014年度國家優(yōu)秀青年科學(xué)基金項目獲得者。獲2013年度教育部自然科學(xué)獎一等獎（第三完成人）。1995年9月到2005年6月，就讀于北京大學(xué)數(shù)學(xué)科學(xué)學(xué)院，獲理學(xué)學(xué)士和博士學(xué)位（碩博連讀）；2004年1月到2006年12月，工作于德國馬普計算機科學(xué)研究所。

他主要在混成系統(tǒng)自動驗證、微分方程和動力系統(tǒng)、符號-數(shù)值計算、計算復(fù)雜性、空間非開普勒軌道分析與優(yōu)化控制等領(lǐng)域從事基礎(chǔ)和應(yīng)用研究。博士期間，在導(dǎo)師鄭志明教授的指導(dǎo)下，提出了偽除機理論，從而推廣了Smale等提出的著名的BSS機器(即所謂的實圖靈機模型)，并在2002年國際數(shù)學(xué)家大會分會場做此研究成果的報告。以此為基礎(chǔ)，在實代數(shù)系統(tǒng)的研究上也取得了一系列原創(chuàng)成果。Herbrand獎得主、德國馬普計算機科學(xué)研究所前所長H.Ganzinger教授高度重視，特意邀請他前往德國馬普計算機科學(xué)研究所做短期訪問；隨后，在未取得博士學(xué)位情況下，他被破格邀請到馬普從事博士后研究，并進入德國大型跨區(qū)域科研項目AVACS（www.avacs.org）的核心研究小組之中。

在混成系統(tǒng)自動驗證領(lǐng)域，他對非線性混成系統(tǒng)安全性自動驗證問題進行了直接處理，突破了之前理論主要通過線性近似來討論的局限性，并開發(fā)了自動驗證軟件Hsolver（hsolver.sourceforge.net/）。由美國工程院院士Alberto L. Sangiovanni-Vincentelli發(fā)表的、詳細(xì)介紹國際上混成系統(tǒng)研究方面最新進展的綜述性學(xué)術(shù)論文《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”。
歸國后，他把混雜(成)系統(tǒng)引入到空間非開普勒軌道的分析與優(yōu)化控制之中，被譽為“從混雜系統(tǒng)研究空間軌道構(gòu)思新穎，是航天器軌道研究的一個新方向”。發(fā)表在《宇航學(xué)報》的學(xué)術(shù)論文《空間非開普勒軌道分析與控制中的數(shù)學(xué)問題》被西北工業(yè)大學(xué)精品課程《航天器飛行力學(xué)》列為學(xué)科前沿（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等領(lǐng)域國際頂級刊物和AAAI、CAV、ISSAC、HSCC等領(lǐng)域國際頂級會議上發(fā)表學(xué)術(shù)論文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、日本早稻田大學(xué)、新加坡國立大學(xué)、清華大學(xué)、CNRS、INRIA、MPII、中國科學(xué)院軟件所等國內(nèi)外著名機構(gòu)的學(xué)者他引300余次，單篇最高他引90余次。特別地，圖靈獎得主Edmund M. Clarke、美國工程院院士Alberto L. Sangiovanni-Vincentelli、美國工程院院士、歐洲科學(xué)院院士Moshe Y. Vardi、歐洲科學(xué)院院士Marta Kwiatkowska、清華大學(xué)孫家廣院士、斯坦福大學(xué)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等給予了積極的正面評價，諸如“明顯優(yōu)勢”、“極大改進”、“靈感之源”等等。

自2007年以來承擔(dān)科研項目情況：

1）參與973項目“海量信息的協(xié)同性和可生存性的理論與實踐研究”的“海量信息系統(tǒng)協(xié)同性和可生存性的隨機模型研究”課題組(2005CB321902，2006-2010)。

2）主持2007年度北京市優(yōu)秀人才資助項目“混雜系統(tǒng)自動驗證和分析”(2007.01-2008.12)；

3）主持教育部留學(xué)歸國人員科研啟動基金“混雜系統(tǒng)自動驗證與分析”(2008.01-2009.12)；

4）主持國家軍口863項目“XXXXXXXXXXXXXXXX關(guān)鍵技術(shù)研究”(2008.07-2010.06，70萬)；

5）主持2008年度北京市科技新星計劃項目“混雜系統(tǒng)自動驗證及其在軟件可靠性中的應(yīng)用”(2009.01-2011.12，25萬)；

6）主持國家軍口863項目“XXXXXXXXXXXXXX可靠性研究”(2010.07-2011.06，30萬)；

7）主持國家自然基金項目“基于代數(shù)分析與符號計算的混成系統(tǒng)自動驗證”（2011.01-2013.12，20萬）；

8）主持軟件開發(fā)環(huán)境國家重點實驗室自選課題“基于微分不變量的混成系統(tǒng)安全性自動驗證”（2011.05-2013.05,15萬）；

9）主持北航領(lǐng)航基金“海量信息知識體系發(fā)現(xiàn)與進化中的關(guān)鍵問題研究”(2011.01-2011.12,10萬)。

任現(xiàn)職以來發(fā)表的代表性論文：

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為計算機科學(xué)“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為計算機科學(xué)“Programming Languages and Software Engineering”的頂級會議)（Scholar google 搜索結(jié)果，9次引用）

11) 薛白，佘志坤，余婧，劉鐵鋼，鄭志明�；诨祀s系統(tǒng)的空間飛行器懸�？刂啤Ｖ袊臻g科學(xué)技術(shù)。第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) 佘志坤，薛白，叢源良，劉鐵鋼，鄭志明。最優(yōu)雙沖量交會問題的數(shù)學(xué)建模與數(shù)值求解。宇航學(xué)報。第31卷，第1期，pp. 155-161, 2010.

8) 裴森，孫野，趙珍，王海濤，余志坤. 一類一維混沌映射的拓?fù)錀l件。第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非開普勒軌道分析與控制中的數(shù)學(xué)問題。宇航學(xué)報。第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.

任現(xiàn)職之前的代表性論文（與博士后合作導(dǎo)師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 搜索結(jié)果，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 搜索結(jié)果，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 搜索結(jié)果，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.