施智平，工学博士，教授，博士生导师，首都师范大学信息工程学院院长，电子系统可靠性技术北京市重点实验室主任。研究兴趣包括形式化验证，机器视觉，人工智能。
主要经历
2013.1-2014.1，美国波特兰州立大学，访问；
2011.7-2011.8，访问加拿大Concordia大学HVG实验室；
2010.10-现在，首都师范大学信息工程学院，教授；
2005.7-2010.9，中国科学院计算技术研究所智能信息处理重点实验室，副研究员；
2002.9-2005.6，中国科学院 计算技术研究所读博，计算机软件与理论专业，导师为史忠植研究员；
中国计算机学会高级会员，人工智能学会、ACM、IEEE 会员，计算机学会形式化专委会委员；曾任International Conference on Intelligent Information Processing、 the 19th ACS Australian Joint Conference on Artificial Intelligence程序委员；担任Multimedia Tools and Applications、The International Journal of Computational Intelligence Systems、Journal of Engineering and Computer Innovations、Informatica、Computers & Mathematics with Applications、中国科学、计算机学报、软件学报、电子学报、计算机辅助设计与图形学学报等期刊审稿专家。共（合作）发表学术论文100多篇。
2006年获北京市科学技术奖三等奖；2011年、2017年两次获北京市科学技术奖二等奖；2012年北京市优秀人才培养资助项目D类；2013年北京市高校青年拔尖人才；2008 年获中国科学院计算技术研究所“优秀研究人员”称号。
轻型工业机器人与安全验证北京市重点实验室是美国教授和首师大组成的联合实验室，研究智能机器人、机器视觉、虚拟现实、操作系统、形式化验证等技术。机器人技术是人工智能和先进制造技术的结合，是当前和未来社会最重要的革命性技术，欢迎有激情肯努力的同学报考研究生。这里提供国家级项目课题，机器人、机器视觉、VR/AR、深度学习工作站等优越的实验设备，参加全国各地暑期学校的机会，国际交流的机会。
主持项目
国家自然科学基金，拉格朗日动力学形式化及其在机器人验证中的应用，**， 2019.1-2022.12；
国家重点研发计划项目子课题：伤员救援机器人控制器嵌入式设计及软件可靠性分析，2017.7-2020.6；
国家自然科学基金：机器人运动学形式化分析及其算法验证，**，2015.1-2018.12；
中澳两国政府间国际科技合作计划"系统形式化验证及性能分析关键技术合作研究",2012-2014；合作主持
国家自然科学基金：希尔伯特空间以及矩阵理论在HOL4中的形式化，**，2012-2015；
国家自然科学基金：基于视感知的图像视频语义获取关键技术研究，**，2010-2012；
计算机体系结构国家重点实验室开放课题：矩阵在高阶逻辑定理证明器中的形式化，2011.10-2013.10；
参加项目
中加两国政府间国际科技合作计划"苛刻环境嵌入式系统高可靠串行通信抗干扰机制及验证",2010-2012；
国家自然科学基金重点项目“基于云计算的海量数据挖掘”，No.**, 2011.1-2014.12；
973项目子课题“非结构化信息(图像)的内容理解与语义表征”No.2007CB311004，2007.7-2012.7；
国家自然科学基金“基于感知学习和语言认知的智能计算模型研究”No.**，2005.1-2008.12；
国家“八六三”高技术研究发展计划“基于感知机理的智能信息处理技术”, 2006.9-2008.12
研究兴趣
定理证明，形式化验证，机器人运动特性形式化分析
图像视频内容理解，三维视觉、VR/AR
人工智能+教育
专著
《机器学习——算法背后的理论与优化》，作者:史春奇，卜晶祎，施智平，清华大学出版社，2019年6月出版
专著学术论文
2019
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 ( SCI IF 5.785 ) Pub Date : 2019-08-18 , DOI: 10.1016/j.neunet.2019.07.010.
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)
Rongbo Zhao, Zhiping Shi, Yong Guan*, Zhenzhou Shao*, Qianying Zhang, Guohui Wang Inverse kinematic solution of 6R robot manipulators based on screw theory and the Paden–Kahan subproblem. December 27, 2018. International Journal of Advanced Robotic Systems. https://doi.org/10.1177/**18297.(SCI) Volume: 15 issue: 6
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 1.405
Liming Li, Zhiping Shi*, Yong Guan, Qianying Zhang, Yongdong Li. Formalization of geometric algebra in HOL Light. Journal of Automated Reasoning (2018). https://doi.org/10.1007/s10817-018-9498-9.(SCI, CCF B)
2018
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)
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
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
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. FR3LO
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
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类)
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类推荐)
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)
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
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 EB1BN，IF 0.905)
马莎,施智平,李黎明,关永,张杰, Xiaoyu SONG.几何代数的高阶逻辑形式化.软件学报,2016,27(3):497?516. http://www.jos.org.cn/1000-9825/4977.htm (EI20**3)
马莎;施智平*;关永;李黎明;邵振洲;张杰. 共形几何代数与机器人运动学的形式化. 小型微型计算机系统，2016,37(3).555-561
杨秀梅, 关永*, 施智平,吴爱轩, 张倩颖, 张杰. 函数矩阵及其微积分的高阶逻辑形式化. 计算机科学. 2016, 43(11):24-29。
李姗姗,赵春娜,关永,施智平,王瑞,李晓娟,叶世伟.分数阶微积分定义的一致性在HOL4中的验证[J]. 计算机科学, 2016, 43(3):23-26.
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
杨秀梅;施智平*;吴爱轩;关永;叶世伟;张杰. 串联机器人雅可比矩阵的高阶逻辑形式化，小型微型计算机系统，2016,37(4):726-731
2015
李志欣, 施智平, 张灿龙, 王金艳. 混合生成式和判别式模型的图像自动标注[J]. 中国图象图形学报，2015,20(5):0687-0699.
安育龙, 施智平, 叶世伟, 李晓娟, 关永, 张杰, 魏洪兴. GJK算法的一种特殊情形的形式化验证和应用[J]. 小型微型计算机系统, 2015(02):365-369.
黎向阳, 吴敏华, 施智平. 基于Gabor变换域的积分直方图鞋印图像检索[J]. 计算机应用与软件. 2015,32(3):215－219
2014
Zhiping Shi, Zhenke Liu, Yong Guan, Shiwei Ye, Jie Zhang, and Hongxing Wei, “Formalization of Function Matrix Theory in HOL,” Journal of Applied Mathematics, vol. 2014, Article ID 201214, 10 pages, 2014.doi:10.1155/2014/201214 (July,24) AR3AY
Zhiping Shi, Yan Zhang, Zhenke Liu, Xinan Kang, Yong Guan, Jie Zhang, Xiaoyu Song. Formalization of Matrix Theory in HOL4. Advances in Mechanical Engineering. vol. 2014, Article ID 195276, 16 pages, 2014. doi:10.1155/2014/195276. (Aug. 28) SCI: AS4RD
Liming Li; Zhiping Shi; Yong Guan; Chunna Zhao; Jie Zhang; Hongxing Wei, Formal verification of a collision-free algorithm of dual-arm robot in HOL4, Robotics and Automation (ICRA), 2014 IEEE International Conference on , pp.1380-1385, May 31 2014-June 7 2014 doi: 10.1109/ICRA.2014.**
Xiangyang Li, Shuqiang Jiang, Xinhang Song, Luis Herranz, Zhiping Shi. Multipath Convolutional-Recursive Neural Networks for Object Recognition. Intelligent Information Processing VII IFIP Advances in Information and Communication Technology Volume 432, 2014, pp 269-277. Hangzhou, China, October 17-20, 2014
Xiangyang Li, Minhua Wu, Zhiping Shi.The Retrieval of Shoeprint Images Based on the Integral Histogram of the Gabor Transform Domain. Intelligent Information Processing 2014: 249-258.Hangzhou, China, October 17-20, 2014
Liming Li, Zhiping Shi, Yong Guan, Jie Zhang and Hongxing Wei. Formalizing the Matrix Inversion Based on the Adjugate Matrix in HOL4.Intelligent Information Processing VII, IFIP Advances in Information and Communication Technology Volume 432, 2014, pp 178-186. Hangzhou, China, October 17-20, 2014
Liu, Xi; Shi, Zhi-Ping; Shi, Zhong-Zhi. A co-boost framework for learning object categories from Google Images with 1st and 2nd order features. Visual Computer, 30(1):5-17, January 2014. EI, SCI
安育龙, 施智平, 叶世伟, 李晓娟, 关永, 张杰, 魏洪兴. 一个空间线段距离算法的形式化和应用.第八届全国测试学术会议,武汉，2014年7月18-20日
康西楠，施智平，叶世伟，关永. 矩阵变换理论在hol4中的形式化. 计算机仿真. 2014, 31(3):289-294
2013
Zhiping Shi, Weiqing Gu, Xiaojuan Li, Yong Guan, Shiwei Ye and Jie Zhang. The Gauge Integral Theory in HOL4. Journal of Applied Mathematics, vol. 2013, Article ID 160875, 7 pages, 2013. doi:10.1155/2013/160875 (SCIE索引144ET)
Zhiping Shi, Liming Li, Yong Guan, Xiaoyu Song, Minhua Wu, Jie Zhang. Formalization of the Complex Number Theory in HOL4. Applied Mathematics & Information Science. 2013,7(1):279-286.
Yupeng Zhang, Zhiping Shi, Yong Guan, Xiaojuan Li, Jie Zhang. Formal Verification for SpaceWire Decoding by Appling Theorem Proving. SpaceWire 2013.189-192. International SpaceWire Conference 2013,10 - 14 June, Gothenburg.
张玉鹏,施智平,关永,李黎明,赵春娜,张杰. SpaceWire译码电路在HOL4中的形式化验证. 小型微型计算机系统，2013, 34(8):1959-1963
刘振科，施智平，关永，金声震，张杰，叶世伟，李晓娟。函数矩阵理论在HOL4中的形式化。小型微型计算机系统，2013,34(3):654 - 658
谷伟卿，施智平，关永，张杰，赵春娜，叶世伟。Gauge积分在HOL4中的形式化[J].计算机科学,2013,40(2):191-194.228
李志欣，施智平，陈宏朝，吴璟莉. 基于语义学习的图像多模态检索. 计算机工程. 2013,39(3):258-263
2012
施智平，李清勇，赵晓东，何清，史忠植。基于内容图像检索中的优化鉴别特征.计算机辅助设计与图形学学报，2012,24(12): 1592-1598
李黎明，关永，吴敏华，张杰，施智平。运用定理证明的形式化方法验证SpaceWire编码电路。小型微型计算机系统，2012,33(6): 1372-1376
Zhiping Shi, Xi Liu, Qingyong Li, Qing He, Zhongzhi Shi. Extracting Discriminative Features for CBIR. Multimedia tools and application. 2012,61(2): 263-279.doi:10.1007/s11042-011-0836-8. (SCI、EI)
2011
Zhiping Shi, Xi Liu, Qingyong Li, Qing He, Zhongzhi Shi. Extracting Discriminative Features for CBIR. Multimedia tools and application. 2012,61(2): 263-279.doi:10.1007/s11042-011-0836-8. (SCIE、EI检索源刊)
Zhiping SHI, Zhiquan DAI, Yong GUAN, Minhua WU, Shengzhen JIN, Jie ZHANG, Xiaojuan LI. Systematic Verification of SpaceWire Bus with Model Checking. SpaceWire-2011 Proceedings of International SpaceWire Conference, San Antonio, Nov. 8-10, 2011, ISBN: 978-0-**-3-9,pp240-247.
Zhi Quan Dai, Yong Guan, Sheng Zhen Jin, Zhi Ping Shi, Xiao Juan Li, Jie Zhang. SpaceWire State Machine Verification Based on Model Checking. 2011, Applied Mechanics and Materials. 55-57(2011):2192-2196.
Xi Liu, Zhiping Shi, Zhongzhi Shi. Model shared semi-supervised learning for multi-label image. ICIP2011
Li Zhixin, Shi Zhiping, Liu Xi, Shi Zhongzhi. Modeling continuous visual features for semantic image annotation and retrieval [J]. Pattern Recognition Letters (PRL). 32(3): 516-523 (2011)（SCI、EI检索）
李志欣，施智平, 李志清, 史忠植. 融合语义主题的图像自动标注[J]. 软件学报. 2011,22(4):801-812 (EI)
2010
Xi Liu, Zhiping Shi, Zhixin Li, Xishun Wang, Zhongzhi Shi. Sorted Label Classifier Chains for Learning Images with Multi-label. ACM MM 2010. 951-954
Zhixin Li; Zhiping Shi; Xi Liu; Zhiqing Li; Zhongzhi Shi. Fusing Semantic Aspects for Image Annotation and Retrieval. Journal of Visual Communication and Image Representation. 2010, 21(8):798–805 (SCI、EI检索)
Xi Liu, Zhiping Shi, Zhixin Li, Xishun Wang, Zhongzhi Shi. Sorted Label Classifier Chains for Learning Images with Multi-label. ACM MM 2010. ACCEPTED
Zhixin Li; Zhiping Shi; Xi Liu; Zhiqing Li; Zhongzhi Shi. Fusing Semantic Aspects for Image Annotation and Retrieval. Journal of Visual Communication and Image Representation. 2010, 21(8):798–805
李志清,施智平,李志欣,史忠植 基于结构相似度的稀疏编码模型 软件学报 2010,21(10):2410-2419，(EI源)。
李志清, 施智平, 李志欣, 史忠植. 结构相似度稀疏编码及其图像特征提取[J]. 模式识别与人工智能, 2010, 23(1): 17–22
刘曦, 史忠植, 石志伟, 施智平. 一种基于特征捆绑计算模型的物体识别方法. 软件学报, 2010,21(3):452?46. (EI)
Qingyong Li, Zhiping Shi: Texture image retrieval using compact texton co-occurrence matrix descriptor. Multimedia Information Retrieval 2010: 83-90
Zhixin Li, Zhiping Shi, Xi Liu, Zhongzhi Shi. AUTOMATIC IMAGE ANNOTATION WITH CONTINUOUS PLSA. ICASSP 2010. 806–809 Lecture
Zhiqing Li, Zhiping Shi, Xi Liu, Zhongzhi Shi. A NOVEL SPARSE CODING MODEL BASED ON STRUCTURAL SIMILARITY. ICASSP 2010. 4170-4173.Poster
课题组研究生
在读博士生(导师关永教授)：张景芝，王国辉, 吴爱轩
在读硕士生(包括合作指导)：
2017级：陈琦，陈善言，聂玉涵，温兴森，付超凡，吴爽；
2018级：康泽岩，董璐，刘鹏，潘健；王畅，汪澍，张诗雨；
已毕业研究生：
李黎明：几何代数的形式化及其在机器人学中的形式化建模，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月答辩。
相关链接
http://www.cl.cam.ac.uk/research/hvg/about.html
http://hvg.ece.concordia.ca/
http://symbolaris.com/meta/andre.html
http://formes.asia/cms/index
http://www-sop.inria.fr/members/Yves.Bertot/research.html
http://shemesh.larc.nasa.gov/fm/fm-main-research.html
中科院计算所 智能科学课题组
Computer Vision Homepage at CMU. Lots of good stuff here.
CVonline: heaps of tutorials and info about various computer vision techniques.
http://csnet.otago.ac.nz/cosc453/ some good vision tutorials
http://www.eucognition.org/ecvision/education/On-line_Cognitive_Vision_Course.htm
http://www.kernel-machines.org/tutorial.html
研究生指南：http://www.cs.ucla.edu/~palsberg/azuma.html
形式化方法会议：http://user.it.uu.se/~bengt/Info/conferences.shtml
论文写作心得：http://www.seekbio.com/biotech/study/wskill/2011/z**.html
照片

施智平最近修改于2019年8月22日
Copyright ? 2019-2022. 首都师范大学 信息工程学院
轻型工业机器人与安全验证北京市重点实验室
高可靠嵌入式系统北京市工程研究中心
电子系统可靠性技术北京市重点实验室