查看导师信息

导师姓名施智平---副研究员
导师性别男
政治面貌群众
联系电话68906706
通讯地址北京市西三环北路56号
邮政编码100048
E-Mailshizhiping@gmail.com。
主页地址http://www.hresc.cn
工作简历2005-2010年，中科院计算所，助理研究员，副研究员2010-现在，首师大信息工程学院，副研究员2011.7-2011.8，加拿大Concordia大学，访问学者2013.1-2014.1，美国波特兰州立大学，访问学者
教学工作计算机图形学
研究领域形式化验证，定理证明，矩阵理论形式化，视觉信息分析随着现代信息技术的发展，信息系统的规模越来越大，设计的复杂度越来越高。由于系统故障造成的国民经济和国家战略任务的损失也越来越严重。系统的验证过程所耗费的经费和时间也越来越高。据统计，大型系统，如哈勃望远镜、GPS和载人航天的验证经费和时间都占到整个工程周期的50%-80%。传统的模拟和仿真验证利用大量的测试例来分析系统行为推理性质，因其简单易行至今仍是主流的方法。但是它们都有先天缺陷??非完备性。对复杂的系统，穷尽的测试是不可能的，因此这些方法只能证明有错而不能证明无错。信息技术的发展迫切需要更好的验证方法和工具。形式化验证采用基于数学推理与演绎的方法来论证系统的正确性，具有传统模拟、仿真技术无法比拟的完备性、精准性的优势。形式化验证主要有三种方法：等价性检验，模型检验和定理证明。等价性验证最为成熟，已经成为一种事实工业标准，几乎所有的电子设计自动化(ElectronicDesignAutomation)供应商都提供这种工具，主要用于验证一个设计在不同层次或变换前后其功能是否一致。模型检验方法在软硬件设计中都取得巨大成功，主要优点是完全自动化和能够给出验证的反例，状态爆炸问题是模型检验方法中研究的主要问题。机器定理证明是把人证明数学定理和日常生活中的演绎推理变成一系列能在计算机上自动实现的符号演算的过程和技术，又称自动定理证明和自动演绎。定理证明方法可以用于任何能被数学模型表示的系统，不受状态数限制，是非常理想的验证方法。证明过程需要专家指导，建模和推理能力依赖定理证明器中已有的公理和已经证明的定理。定理证明器包含的定理库越多，其推理能力越强，对专家指导的依赖也就越小，因此定理库的构建成为定理证明应用的关键问题。
在研课题主持国家自然科学基金2项：基于视感知的图像视频语义获取关键技术研究，No.60903141，2010-2012；希尔伯特空间以及矩阵理论在HOL4中的形式化，No.61170304，2012-2015；合作主持中澳两国政府间国际科技合作计划"系统形式化验证及性能分析关键技术合作研究",2012-2014；主持计算机体系结构国家重点实验室开放课题“矩阵在高阶逻辑定理证明器中的形式化”，CARCH201102参加项目：参加中加两国政府间国际科技合作计划"苛刻环境嵌入式系统高可靠串行通信抗干扰机制及验证",2010-2012；国家自然科学基金重点项目“基于云计算的海量数据挖掘”，No.61035003,2011.1-2114.12973项目子课题“非结构化信息(图像)的内容理解与语义表征”No.2007CB311004，2007.7-2012.7
科研成果在视觉信息分析与检索和形式化验证领域（合作）发表论文50多篇，其中SCI6篇，EI40多篇。
著译目录[1]ZhipingShi,WeiqingGu,XiaojuanLi,YongGuan,ShiweiYeandJieZhang.TheGaugeIntegralTheoryinHOL4.JournalofAppliedMathematics.Accepted(SCIE)[2]ZhipingShi,LimingLi,YongGuan,XiaoyuSong,MinhuaWu,JieZhang.FormalizationoftheComplexNumberTheoryinHOL4.AppliedMathematics&InformationScience.Accepted.(SCIE)[3]YupengZhang,ZhipingShi,FormalVerificationforSpaceWireDecodingbyApplingTheoremProving.SpaceWire2013.Accepted[4]张玉鹏,施智平,关永,李黎明,赵春娜,张杰.SpaceWire译码电路在HOL4中的形式化验证.小型微型计算机系统，2013.3录用[5]刘振科，施智平，关永，金声震，张杰，叶世伟，李晓娟。函数矩阵理论在HOL4中的形式化。小型微型计算机系统，2012.5录用[6]谷伟卿，施智平，关永，张杰，赵春娜，叶世伟。Gauge积分在HOL4中的形式化。计算机科学，2012.8录用[7].ZhipingShi,XiLiu,QingyongLi,QingHe,ZhongzhiShi.ExtractingDiscriminativeFeaturesforCBIR.Multimediatoolsandapplication.Accepted(SCIE、EI检索源刊)[8]ZhipingSHI,ZhiquanDAI,YongGUAN,MinhuaWU,ShengzhenJIN,JieZHANG,XiaojuanLI.SystematicVerificationofSpaceWireBuswithModelChecking.SpaceWire2011.Accepted.[9]QingyongLi,ZhipingShi.AHigherOrderContextualTextureDescriptorforImageRetrievalUsingGeneralizedTextonCo-occurrenceMatrix.WillbepublishedinVol.15,No.7ofthejournalINFORMATION.(SCIE、EI检索源刊)[10]ZhiQuanDai,YongGuan,ShengZhenJin,ZhiPingShi,XiaoJuanLi,JieZhang.SpaceWireStateMachineVerificationBasedonModelChecking.2011,AppliedMechanicsandMaterials.55-57(2011):2192-2196.[11]ZhixinLi;ZhipingShi;XiLiu;ZhiqingLi;ZhongzhiShi.FusingSemanticAspectsforImageAnnotationandRetrieval.JournalofVisualCommunicationandImageRepresentation.2010,21(8):798?805(SCI、EI检索)[12]XiLiu,ZhipingShi,ZhongzhiShi.Modelsharedsemi-supervisedlearningformulti-labelimage.ICIP2011[13]LiZhixin,ShiZhiping,LiuXi,ShiZhongzhi.Modelingcontinuousvisualfeaturesforsemanticimageannotationandretrieval[J].PatternRecognitionLetters(PRL).32(3):516-523(2011)（SCI、EI检索）
获奖荣誉2006年度北京市科学技术奖三等奖2008年度中科院计算所优秀研究人员2011年度北京市科学技术奖二等奖2012年北京市优秀人才培养资助D类项目2012年北京市属高校青年拔尖人才
主要兼职担任MultimediaToolsandApplications、InternationalJournalofComputationalIntelligenceSystems、计算机学报、软件学报、电子学报、计算机辅助设计与图形学学报等期刊审稿专家
备注课题组与加拿大Concordia大学Tahar教授、美国波特兰大学宋晓宇教授、澳大利亚新南威尔士大学薛京灵教授、香港理工大学邵子力教授合作研究，已经和香港理工大学、Concordia大学联合培养多名研究生。招收形式化验证和图像处理方向的研究生，欢迎计算机相关专业、应用数学、通信工程等专业学生报考。