施智平，博士，教授，博士生导师，yl9193永利经理，电子系统可靠性技术北京市重点实验室主任。
主要经历：
2013.1-2014.1，美国波特兰州立大学，访问学者；
2011.7-2011.8，访问加拿大Concordia大学HVG实验室；
2010.10-现在，yl9193永利，教授；
2005.7-2010.9，中国科学院计算技术研究所智能信息处理重点实验室，副研究员；
2002.9-2005.6，中国科学院 计算技术研究所读博，计算机软件与理论专业；
研究兴趣包括形式化验证，计算机视觉，人工智能，（合作）发表学术论文200多篇，包括IEEE TIP、TDSC、JAR、FAOC、ACM MM、AAAI、CVPR、IJCAI等顶级期刊和会议论文，获得北京市科学技术奖二等奖2次、三等奖1次。中国计算机学会高级会员，人工智能学会、ACM、IEEE 会员，人工智能学会智能服务专委会常委，计算机学会形式化专委会委员、人工智能与模式识别专委会委员，自动化学会模式识别与机器智能专委会委员；全国高等院校计算机基础教育研究会第九届理事会理事；国家自然基金委评审专家。曾任AAAI、Chinasoft、SETTA、International Conference on Intelligent Information Processing等程序委员。
在关键基础软件正确性验证、计算机视觉方向招收研究生，导师组团队指导，欢迎有激情肯努力的同学报考，提供参与国家级项目课题的机会和良好的科研环境，参加全国各地暑期学校的机会、国际交流的机会。
主持项目：
国家航天操作系统形式化验证项目，2022-2023；
国家自然科学基金，拉格朗日动力学形式化及其在机器人验证中的应用，61876111， 2019.1-2022.12；
校交叉团队建设项目：人工智能技术与应用，2019-2021；
校重点研究专题：视觉、语言及其多模态表征学习和课堂教学分析诊断，2019-2022；
国家重点研发计划项目子课题：伤员救援机器人控制器嵌入式设计及软件可靠性分析，2017.7-2020.6；
国家自然科学基金：机器人运动学形式化分析及其算法验证，61472468，2015.1-2018.12；
中澳两国政府间国际科技合作计划：系统形式化验证及性能分析关键技术合作研究，2012-2014；合作主持
国家自然科学基金：希尔伯特空间以及矩阵理论在HOL4中的形式化，61170304，2012-2015；
国家自然科学基金：基于视感知的图像视频语义获取关键技术研究，60903141，2010-2012；
计算机体系结构国家重点实验室开放课题：矩阵在高阶逻辑定理证明器中的形式化，2011.10-2013.10；
研究兴趣
机器定理证明，形式化验证，机器人运动动力学形式化分析
计算机视觉，图像视频内容理解
人工智能+教育
专著
《机器学习——算法背后的理论与优化》，作者:史春奇，卜晶祎，施智平，清华大学出版社，2019年6月出版
《Formalization of Complex Analysis and Matrix Theory》，Shi Zhiping, Guan Yong, Li Ximeng, Tsinghua University Press and Springer Nature Singapore Pte Ltd. 2020. (eBook) https://doi.org/10.1007/978-981-15-7261-6
《几何代数的形式化与初步应用》，关永, 李黎明, 施智平著.北京:科学出版社, 2020.5.
《哈密顿力学理论的形式化与机器人动力学形式化分析》，施智平，王国辉，关永，王瑞.北京：科学出版社. 2022.09
《拉格朗日力学理论的形式化与机器人动力学形式化分析》，关永，张景芝，施智平，李晓娟. 北京：科学出版社. 2022.05
学术论文
2023
1. Yongchun Zhu, Fuzhen Zhuang, Xiangliang Zhang, Zhiyuan Qi, Zhi-Ping Shi, Juan Cao, Qing He:Combat data shift in few-shot learning with knowledge graph. Frontiers Comput. Sci. 17(1): 171305 (2023)
2. Zhilei Li, Jun Li, Yuqing Ma, Rui Wang, Zhiping Shi, Yifu Ding, and Xianglong Liu, Spatio-Temporal Adaptive Network with Bidirectional Temporal Difference for Action Recognition," IEEE Transactions on Circuits and Systems for Video Technology, 2023. CCF B
3. Ximeng Li, Qianying Zhang, Guohui Wang, Zhiping Shi, Yong Guan: A Unified Proof Technique for Verifying Program Correctness with Big-step Semantics. Journal of Systems Architecture, 136: 1-22, 2023. [ CCF B类、SCI 2区期刊 ]
2022
4. J. Li, D. Wang, X. Liu, Z. Shi, M. Wang. Two-Branch Attention Network via Efficient Semantic Coupling for One-Shot Learning. IEEE Transactions on Image Processing, 2022, 31: 341-351, CCF A
5. Jian Deng, Mingyue Li, Yongxin Chen, Zhenzhou Shao, Ying Qu, Yong Guan, Jun Zhang, Zhiping Shi:Cross-Guided Feature Fusion with Intra-Modality Reweighting for Multi-Spectral Pedestrian Detection. ICPR 2022: 4864-4870
6. M. Cheng, Y. Guan, Z. Shi and Wei Song, Unsupervised Multi-view High-Dimensional Data Representation Learning via Weighted Third-order Tensor Analysis, ACM Trans. on Information System, 2022.
7. Zhe Wang, Chenggang Wu, Yinqian Zhang, Bowen Tang, Pen-Chung Yew, Mengyao Xie, Yuanming Lai, Yan Kang, Yueqiang Cheng, Zhiping Shi: Making Information Hiding Effective Again. IEEE Trans. Dependable Secur. Comput. 19(4): 2576-2594 (2022)
8. 李希萌, 王国辉, 张倩颖, 施智平*, 关永. 基于函数式语义的循环和递归程序结构通用证明技术. 软件学报, 在线出版 (2022-03-24).
9. 陈善言,关永*,施智平,王国辉.机器人碰撞检测方法形式化.软件学报,2022,33(6):2246-2263
2021
10. Zhixin Li, Lan Lin, Canlong Zhang, Huifang Ma, Weizhong Zhao, and Zhiping Shi. 2021. A Semi-supervised Learning Approach Based on Adaptive Weighted Fusion for Automatic Image Annotation. ACM Trans. Multimedia Comput. Commun. Appl. 17, 1, Article 37 (April 2021), 23 pages.
11. Xinmei Fu, Zhenzhou Shao*, Ying Qu, yong guan, Yibo Zou, Zhiping Shi, Jindong Tan. Fast and Unsupervised 3D-CNN based Non-Local Feature Learning for Direct Volume Rendering of 3D Medical Images. Conference: 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)
12. 韩宁,李希萌,张倩颖,王国辉,施智平,关永.以太坊中间语言的可执行语义.软件学报,2021,32(6):1717-1732.
13. 芦倩,李晓娟,关永,王瑞,施智平.面向数据流的ROS2数据分发服务形式建模与分析.软件学报,2021,32(6):1818-1829
14. 陆芝浩, 王瑞, 孔辉, 关永, 施智平. Ptolemy离散事件模型形式化验证方法. 软件学报, 2021, 32(6):19.
15. Yong Guan, Jingzhi Zhang, Guohui Wang*, Ximeng Li, Zhiping Shi*, Yongdong Li. Formalization of Euler–Lagrange Equation Set Based on Variational Calculus in HOL Light. Journal of Automated Reasoning (2021) 65:1–29. https://doi.org/10.1007/s10817-020-09549-w【CCF-B】
2020
16. Shanyan Chen, Guohui Wang*, Ximeng Li, Qianying Zhang, Zhiping Shi, Yong Guan. Formalization of Camera Pose Estimation Algorithm based on Rodrigues Formula. Formal Aspects of Computing. 32, 417–437(2020.11.5) CCF-B
17. 王国辉，许京然，刘永梅，施智平*，关永. 摄动开普勒问题形式化建模与验证. 小型微型计算机系统 2020 Vol. 41 (2): 440-444【B类权威核心】
18. 陈琦,王国辉*,张倩颖,施智平,陈善言,关永. 平面并联机构的形式化建模与验证. 小型微型计算机系统.2020 Vol. 41 (5): 925-931 【B类权威核心】
19. S. Zhang, Z. Zhang, F. Zhuang, Z. Shi, X. Han. Compressing Knowledge Graph Embedding with Relational Graph Auto-encoder. The 10th IEEE International Conference on Electronics Information and Emergency Communication, Beijing, China, 2020. EI
20. Zhao Zhang, Fuzhen Zhuang*, Hengshu Zhu, Zhiping Shi, Hui Xiong, Qing He: Relational Graph Neural Network with Hierarchical Attention for Knowledge Graph Completion. AAAI 2020. Feb.7-12, Newyork USA. CCF A
21. Jin, B. , Hu, Y. , Tang, Q. , Niu, J. , Shi, Z. , & Han, Y. , et al. (2020). Exploring spatial-temporal multi-frequency analysis for high-fidelity and temporal-consistency video prediction. CVPR2020, CCF A
22. Yong Guan, Jingzhi Zhang, Guohui Wang, Ximeng Li, Zhiping Shi, Yongdong Li. Formalization of Euler–Lagrange Equation Set Based on Variational Calculus in HOL Light. Journal of Automated Reasonning. 2020(1).
23. GuiluLi, Chang-E Ren, C.L. Philip Chen, Zhiping Shi. Adaptive iterative learning consensus control for second-order multi-agent systems with unknown control gains. Neurocomputing Volume 393, 14 June 2020, Pages 15-26.
2019
24. Yongchun Zhu, Fuzhen Zhuang*, Jindong Wang, Jingwu Chen, Zhiping Shi, Wenjuan Wu, Qing He: Multi-representation adaptation network for cross-domain image classification. Neural Networks 119: 214-221 (2019). CCF B
25. Meiyu Zhang, Qianying Zhang*, Shijun Zhao, Zhiping Shi, Yong Guan. SoftME: A software-based memory protection approach for TEE system to resist physical attacks. Security and Communication Networks, 2019. SCIE
26. X. Li, Z. Shi, Q. Zhang, G. Wang, Y. Guan, N. Han. Towards Verifying Ethereum Smart Contracts at Intermediate Language Level [C]. The 21th International Conference on Formal Engineering Methods (ICFEM), 2019. [录用未发表]
27. Ji D, Zhang Q, Zhao S, Shi Z, Guan Y. MicroTEE: Designing TEE OS Based on the Microkernel Architecture[C]//2019 IEEE TrustCom/BigDataSE, pp.26－33. 5-8 August, 2019 (best paper award) CCF C类
28. Jingzhi Zhang, Guohui Wang*, Zhiping Shi*, Yong Guan, Yongdong Li. Formalization of functional variation in HOL Light. Journal of Logical and Algebraic Methods in Programming. Vol.106, August 2019, Pages 29-38. https://doi.org/10.1016/j.jlamp.2019.04.004. (SCI)0.632
29. 王国辉;许京然;刘永梅;施智平;关永. 基于几何代数的摄动开普勒问题形式化建模与验证. 小型微型计算机系统【录用未发表】
30. 孟子琪, 张倩颖*, 施智平, 关永. 基于可信执行环境的嵌入式双操作系统架构研究. 计算机工程, 2019,45(4):6-12
31. 宋锐, 施智平*, 渠瀛, 邵振洲,关永. 基于深度残差学习的自动驾驶道路场景理解. 计算机应用研究.2019,36(9):2825-2829,2871
32. Chuan Shi, Zhiqiang Zhang, Yugang Ji, Weipeng Wang, Philip S. Yu, Zhiping Shi*. SemRec: a personalized semantic recommendation method based on weighted heterogeneous information. World Wide Web. Jan. 2019, 22(1):153–184. SCI 2.892
33. Liming Li, Zhiping Shi*, Yong Guan, Qianying Zhang, Yongdong Li. Formalization of geometric algebra in HOL Light. Journal of Automated Reasoning. October 2019, 63(3): 787–808. (SCI, CCF B)1.172
34. Y. Nie, Z. Shi, A. Wu, X. Li, G. Wang and Y. Guan. A HOL Theory of the Differential for Matrix Functions[C]. 2019 13th International Symposium on Theoretical Aspects of Software Engineering.Los Alamitos, California:IEEE Computer Society,2019.121-127. Guilin China, 29th-31st July 2019. CCF C类
2018
35. Zhiping Shi, Aixuan Wu, Xiumei Yang, Yong Guan, Yongdong Li, Xiaoyu Song. Formal analysis of the kinematic Jacobian in screw theory. Formal Aspect of Computing. 30(6):739-757. NOV 2018, (SCI HA2VL, CCF B)
36. Guohui Wang, Yong Guan, Zhiping Shi*, Qianying Zhang, Xiaojuan Li and Yongdong Li. Formalization of Symplectic Geometry in HOL-Light. ICFEM 2018. LNCS 11232:270-283
37. Ren C E , Shi Z , Du T . Distributed Observer-Based Leader-Following Consensus Control for Second-Order Stochastic Multi-Agent Systems[J]. IEEE Access, 2018, 6:20077-20084. SCI
38. Qingyong Li, Zhiping Shi, Huayan Zhang, Yunqiang Tan, Shengwei, Ren, Peng Dai, Weiyi Li. A cyber-enabled visual inspection system for rail corrugation. Future Generation Computer Systems, 79(1), pp374-382, February 2018. SCI
39. Kang Yang, Rui Wang*, Yu Jiang, Houbing Song, Chenxia Luo, Yong Guan*,Xiaojuan Li, Zhiping Shi. Sensor attack detection using history based pairwise inconsistency. Future Generation Computer Systems, 86 (2018) 392–402
2017
40. Zhenzhou Shao, Gaoyu Wu, Ying Qu, Zhiping Shi, Yong Guan and Jindong Tan, Robust Principal Component Analysis via Symmetric Alternating Direction for Moving Object Detection, 18th Pacific-Rim Conference on Multimedia, 2017. (CCF-C类)
41. Aixuan Wu, Zhiping Shi*, Xiumei Yang, yong guan, Yong-Dong Li, Xiaoyu Song. Formalization and Analysis of Jacobian Matrix in Screw Theory and Its Application in Kinematic Singularity. Proceeding on 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). pp2835-2842. September 24–28, 2017, Vancouver, BC, Canada. (CCF C类推荐)
42. Yu Hu, Jing Ye, Zhiping Shi*, Xiaowei Li, LAPS: Layout-Aware Path Selection for Post-Silicon Timing Characterization, IEICE TRANS. INF. & SYST., 100(2):323-331 FEBRUARY 2017(SCIE：ES2PP)
43. Zhang, Q., Shi, Z. A new way to prevent UKS attacks using hardware security chips. International Journal of Network Security. 19(5):823-831, 2017.
2016
44. Ma, S., Z. Shi, Z. Shao, Y. Guan, L. Li and Y. Li (2016). Higher-Order Logic Formalization of Conformal Geometric Algebra and its Application in Verifying a Robotic Manipulation Algorithm. Advances in Applied Clifford Algebras. 2016,26(4):1305–1330. DOI: 10.1007/s00006-016-0650-5. First online: 22 March 2016 (SCI)
45. 马莎,施智平,李黎明,关永,张杰, Xiaoyu SONG.几何代数的高阶逻辑形式化.软件学报,2016,27(3):497−516. http://www.jos.org.cn/1000-9825/4977.htm (EI)
46. Li Shanshan, Zhao Chunna, Guan Yong, Shi Zhiping, Li Xiaojuan, Wang Rui, Zhang Qianying. Research on the Higher-order Logic Formalization of Fractance Element[J]. IEEE/CAA Journal of Automatica Sinica, 2016, 13(9):248-256
已毕业研究生：
2020年毕业：陈琦（国务院国有资产监督管理委员会信息中心），陈善言（首都师大读博），聂玉涵（中国工商银行数据中心），温兴森（百度），付超凡（中信银行数据中心），吴爽
李黎明：几何代数的形式化及其在机器人学中的形式化建模，2019博士毕业，中科院软件所博士后；
宋锐：基于深度残差模型的道路分割方法研究，2019年毕业，携程；
唐晨阳：基于生成对抗网络的定理证明步骤选择，2019年毕业，光大银行
许京然：基于几何代数理论的摄动Kepler问题形式化 ，2019年毕业，北京城市学院；
马伟伟：旋量系理论的高阶逻辑形式化，2018年毕业，北京公务员
赵荣波：六自由度串联工业机器人运动学研究，2018年毕业，微电子所读博
孟子琪：嵌入式双操作系统实时性关键技术研究，2018年毕业，人民银行
周生凯：基于深度学习的动力学建模，2018年毕业，IT公司
孙浩然：穿刺机器人运动控制系统的形式化分析与验证，2017年毕业
刘学成：NuttX操作系统任务调度的形式化建模与分析，2017年毕业，欧洲深造
马莎：共形几何代数与机器人运动学的形式化，2016年毕业，爱奇艺；
杨秀梅：串联机器人雅可比矩阵的高阶形式化分析与验证，2016年毕业，中国民航信息集团；
贾娟娟：ROS中XML-RPC协议以及通信模式的形式化验证，2016年毕业，网易；
李姗姗：基于Caputo定义的分数阶微积分高阶逻辑形式化验证，2016年毕业，中国人保财险信息技术部；
周振宇：基于机器视觉的青鳉鱼生物体征监测技术研究，2016年毕业，湖南IT公司；
吴爱轩：旋量理论的形式化及在机器人运动学中的应用，2015年5月答辩。首师大读博
安育龙：基于Hoare逻辑的GJK算法的形式化验证，2015年5月答辩。北理工读博
吕兴利：连续傅里叶变换的高阶逻辑形式化，2015年5月答辩。58同城
赵刚：基于高阶逻辑的拉普拉斯变换形式化建模与验证，2015年5月答辩。国家电网
黎向阳：基于多层次特征学习的图像分类技术研究，2015年毕业，中科院计算所读博
张雁：基于定理证明器HOL的矩阵理论分析与研究，2011年5月答辩，广利核核电站相关验证。
李黎明：代数系统和复数理论的形式化及DS编码器的验证应用，2012年5月答辩。首师大读博。
刘振科：基于定理证明器HOL4的函数矩阵理论的形式化，2013年5月答辩。神州数码。
谷伟卿：基于定理证明器HOL4的gauge积分理论的形式化，2013年5月答辩，广利核核电站相关验证。
张玉鹏：离散傅里叶变换在HOL4中的形式化，2014年5月答辩。上海贝尔。
康西楠：矩阵变换理论在HOL4中的形式化，2014年5月答辩。中国北车。
师丽坤：基于Grünwald-Letnikov定义的分数阶系统形式化分析，2014年5月答辩。
最近修改于2023年4月2日
Copyright © 永利官网 yl9193永利
电子系统可靠性技术北京市重点实验室
轻型工业机器人与安全验证北京市重点实验室
高可靠嵌入式系统北京市工程研究中心