在混成系統自動驗證領域,他對非線性混成系統安全性自動驗證問題進行了直接處理,突破了之前理論主要通過線性近似來討論的局限性,并開發了自動驗證軟件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等給予了積極的正面評價,諸如“明顯優勢”、“極大改進”、“靈感之源”等等。
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次引用)
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.
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.
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.
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.