专任教师

您目前的位置: 首页» 师资队伍» 专任教师» 教授

施智平

 

施智平,博士,教授

首都师范大学 信息工程学院

轻型工业机器人与安全验证北京市重点实验室

电子系统可靠性技术北京市重点实验室

高可靠嵌入式系统北京市工程研究中心

北京市西三环北路56 100048

电话: 86-10-68906706 (实验室)

Email: shizp(at)cnu(dot)edu(dot)cn

 

简介

施智平,工学博士,教授。研究兴趣包括形式化验证,机器视觉,人工智能。

2013.1-2014.1,美国波特兰州立大学,访问学者;

2011.7-2011.8,访问加拿大Concordia大学HVG实验室;

2010.10-现在,首都师范大学信息工程学院,教授;

2005.7-2010.9,中国科学院计算技术研究所智能信息处理重点实验室,副研究员;

2002.9-2005.6中国科学院 计算技术研究所读博,计算机软件与理论专业,导师为史忠植研究员;

中国计算机学会高级会员,人工智能学会、ACMIEEE 会员,计算机学会容错专委会委员;曾任International Conference on Intelligent Information Processing the 19th ACS Australian Joint Conference on Artificial Intelligence程序委员;担任Multimedia Tools and ApplicationsThe International Journal of Computational Intelligence SystemsJournal of Engineering and Computer InnovationsInformaticaComputers & Mathematics with Applications、中国科学、计算机学报、软件学报、电子学报、计算机辅助设计与图形学学报等期刊审稿专家。共(合作)发表学术论文80多篇。

2006 年获北京市科学技术奖三等奖;2011年获北京市科学技术奖二等奖;2012年北京市优秀人才培养资助项目D类;2013年北京市高校青年拔尖人才;2008 年获中国科学院计算技术研究所“优秀研究人员”称号。

轻型工业机器人与安全验证北京市重点实验室是美国教授和首师大组成的联合实验室,研究智能机器人、机器视觉、虚拟现实、操作系统、形式化验证等技术。机器人技术是人工智能和先进制造技术的结合,是当前和未来社会最重要的革命性技术,欢迎有激情肯努力的同学报考研究生。这里提供国家级项目课题,机器人、机器视觉、VR/AR、深度学习工作站等优越的实验设备,参加全国各地暑期学校的机会,国际交流的机会。

项目

主持项目:

1.国家自然科学基金:机器人运动学形式化分析及其算法验证,614724682015.1-2018.12

2.国家自然科学基金:希尔伯特空间以及矩阵理论在HOL4中的形式化,611703042012-2015

3.国家自然科学基金:基于视感知的图像视频语义获取关键技术研究,609031412010-2012

4.计算机体系结构国家重点实验室开放课题:矩阵在高阶逻辑定理证明器中的形式化,2011.10-2013.10

参加项目:

1.中澳两国政府间国际科技合作计划"系统形式化验证及性能分析关键技术合作研究",2012-2014

2.中加两国政府间国际科技合作计划"苛刻环境嵌入式系统高可靠串行通信抗干扰机制及验证",2010-2012

3.国家自然科学基金重点项目“基于云计算的海量数据挖掘”,No.61035003, 2011.1-2014.12

4.973项目子课题非结构化信息(图像)的内容理解与语义表征”No. 2007CB3110042007.7-2012.7

5.国家自然科学基金“基于感知学习和语言认知的智能计算模型研究”No. 604350102005.1-2008.12

6.国家“八六三”高技术研究发展计划“基于感知机理的智能信息处理技术”, 2006.9-2008.12

研究兴趣

数学理论的形式化表达

定理证明,形式化验证

       机器人运动特性形式化分析

       图像视频内容理解,三维视觉、VR/AR

学术论文

2017

1. Yu Hu, Jing Ye, Zhiping Shi*, Xiaowei Li, LAPS: Layout-Aware Path Selection for Post-Silicon Timing Characterization, to be published in IEICE TRANS. INF. & SYST., VOL.E100–D, NO.2 FEBRUARY 2017

2016

2. 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 EB1BNIF 0.905)

3.马莎,施智平,李黎明,关永,张杰, Xiaoyu SONG.几何代数的高阶逻辑形式化.软件学报,2016,27(3):497?516. http://www.jos.org.cn/1000-9825/4977.htm (EI20161902371623)

4.马莎;施智平*;关永;李黎明;邵振洲;张杰共形几何代数与机器人运动学的形式化小型微型计算机系统,2016,37(3).555-561  

5.杨秀梅, 关永*, 施智平,吴爱轩, 张倩颖, 张杰. 函数矩阵及其微积分的高阶逻辑形式化. 计算机科学. 2016, 43(11):24-29

6.李姗姗,赵春娜,关永,施智平,王瑞,李晓娟,叶世伟.分数阶微积分定义的一致性在HOL4中的验证[J]. 计算机科学, 2016, 43(3):23-26.

7. 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

8.杨秀梅;施智平*;吴爱轩;关永;叶世伟;张杰串联机器人雅可比矩阵的高阶逻辑形式化,小型微型计算机系统,2016,37(4):726-731

2015

9.李志欣, 施智平, 张灿龙, 王金艳. 混合生成式和判别式模型的图像自动标注[J]. 中国图象图形学报,2015,20(5):0687-0699.

10.安育龙, 施智平, 叶世伟, 李晓娟, 关永, 张杰, 魏洪兴. GJK算法的一种特殊情形的形式化验证和应用[J]. 小型微型计算机系统, 2015(02):365-369.

11.黎向阳, 吴敏华, 施智平. 基于Gabor变换域的积分直方图鞋印图像检索[J]. 计算机应用与软件. 2015,32(3):215219

2014

12. 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

13. 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

14. 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.6907032

15. 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

16. 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

17. 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

18. 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

19.安育龙, 施智平, 叶世伟, 李晓娟, 关永, 张杰, 魏洪兴. 一个空间线段距离算法的形式化和应用.第八届全国测试学术会议,武汉,2014718-20

20.康西楠,施智平,叶世伟,关永. 矩阵变换理论在hol4中的形式化. 计算机仿真. 2014, 31(3):289-294

2013

21. 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)

22. 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.

23. 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.

24.张玉鹏,施智平,关永,李黎明,赵春娜,张杰. SpaceWire译码电路在HOL4中的形式化验证. 小型微型计算机系统,2013, 34(8):1959-1963

25.刘振科,施智平,关永,金声震,张杰,叶世伟,李晓娟。函数矩阵理论在HOL4中的形式化。小型微型计算机系统,2013,34(3):654 - 658

26.谷伟卿,施智平,关永,张杰,赵春娜,叶世伟。Gauge积分在HOL4中的形式化[J].计算机科学,2013,40(2):191-194.228

27.李志欣,施智平,陈宏朝,吴璟莉. 基于语义学习的图像多模态检索. 计算机工程. 2013,39(3):258-263

2012

28.施智平,李清勇,赵晓东,何清,史忠植。基于内容图像检索中的优化鉴别特征.计算机辅助设计与图形学学报,2012,24(12): 1592-1598

29.李黎明,关永,吴敏华,张杰,施智平。运用定理证明的形式化方法验证SpaceWire编码电路。小型微型计算机系统,2012,33(6): 1372-1376

30. 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. (SCIEI)

2011

31. 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. (SCIEEI检索源刊)

32. 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-9557196-3-9,pp240-247.

33. 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.

34. Xi Liu, Zhiping Shi, Zhongzhi Shi. Model shared semi-supervised learning for multi-label image. ICIP2011

35. 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)SCIEI检索)

36.李志欣,施智平, 李志清, 史忠植. 融合语义主题的图像自动标注[J]. 软件学报. 2011,22(4):801-812 (EI)

2010

37. 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

38. 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):798805 (SCIEI检索)

39. Xi Liu, Zhiping Shi, Zhixin Li, Xishun Wang, Zhongzhi Shi. Sorted Label Classifier Chains for Learning Images with Multi-label. ACM MM 2010. ACCEPTED

40. 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):798805

41.李志清,施智平,李志欣,史忠植  基于结构相似度的稀疏编码模型 软件学报 2010,21(10):2410-2419(EI)

42.李志清, 施智平, 李志欣, 史忠植. 结构相似度稀疏编码及其图像特征提取[J]. 模式识别与人工智能, 2010, 23(1): 17–22

43.刘曦, 史忠植, 石志伟, 施智平. 一种基于特征捆绑计算模型的物体识别方法. 软件学报, 2010,21(3):452?46. (EI)

44. Qingyong Li, Zhiping Shi: Texture image retrieval using compact texton co-occurrence matrix descriptor. Multimedia Information Retrieval 2010: 83-90

45. Zhixin Li, Zhiping Shi, Xi Liu, Zhongzhi Shi. AUTOMATIC IMAGE ANNOTATION WITH CONTINUOUS PLSA. ICASSP 2010. 806–809 Lecture

46. Zhiqing Li, Zhiping Shi, Xi Liu, Zhongzhi Shi. A NOVEL SPARSE CODING MODEL BASED ON STRUCTURAL SIMILARITY. ICASSP 2010. 4170-4173.Poster

 

课题组研究生

在读博士生(导师关永教授):李黎明,张景芝,王国辉吴爱轩

在读硕士生:

  • 2012级:吴爱轩,安育龙,吕兴利,赵刚
  • 2013级:马莎,贾娟娟,杨秀梅,李珊珊
  • 2014级:孙浩然,刘学成,任龙
  • 2015级:孟子琪,马伟伟,赵荣波,周生凯
  • 2016级:许京然,唐晨阳,朱晓霞,宋锐,原嘉琦,张美玉

已毕业研究生:

  • 吴爱轩:旋量理论的形式化及在机器人运动学中的应用,20155月答辩。首师大读博
  • 安育龙:基于Hoare逻辑的GJK算法的形式化验证,20155月答辩。北理工读博
  • 吕兴利:连续傅里叶变换的高阶逻辑形式化,20155月答辩。58同城
  • 赵刚:基于高阶逻辑的拉普拉斯变换形式化建模与验证,20155月答辩。国家电网
  • 黎向阳:基于多层次特征学习的图像分类技术研究,2015年毕业,中科院计算所读博
  • 马莎:共形几何代数与机器人运动学的形式化,2016年毕业,爱奇艺
  • 杨秀梅:串联机器人雅可比矩阵的高阶形式化分析与验证,2016年毕业,中国民航信息集团
  • 贾娟娟:ROSXML-RPC协议以及通信模式的形式化验证,2016年毕业,网易科技
  • 李姗姗:基于Caputo定义的分数阶微积分高阶逻辑形式化验证,2016年毕业,中国人保财险信息技术部
  • 周振宇:基于机器视觉的青鳉鱼生物体征监测技术研究,2016年毕业,湖南
  • 张雁:基于定理证明器HOL的矩阵理论分析与研究,20115月答辩,广利核 核电站相关验证。
  • 李黎明:代数系统和复数理论的形式化及DS编码器的验证应用,20125月答辩。首师大读博。
  • 刘振科:基于定理证明器HOL4的函数矩阵理论的形式化,20135月答辩。神州数码。
  • 谷伟卿:基于定理证明器HOL4gauge积分理论的形式化,20135月答辩,广利核核电站相关验证。
  • 张玉鹏:离散傅里叶变换在HOL4中的形式化,20145月答辩。上海贝尔。
  • 康西楠:矩阵变换理论在HOL4中的形式化,20145月答辩。中国北车。
  • 师丽坤:基于Grünwald-Letnikov定义的分数阶系统形式化分析,20145月答辩。

相关链接

http://www.hresc.cn

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/z8211697.html

 

 

施智平最近修改于2017322

Copyright ? 2015-2018. 首都师范大学 信息工程学院

轻型工业机器人与安全验证北京市重点实验室

高可靠嵌入式系统北京市工程研究中心

电子系统可靠性技术北京市重点实验室