【人物简介】

　　张海宾，1982年出生于山东菏泽，2003年本科毕业于中国海洋大学，随后考入西安电子科技大学攻读硕士学位，2004年直博，2007年获得工学博士学位留校任教，2010年晋升副教授，硕士生导师。

【研究方向】

1. 高可信软件技术 2. 图形图像相关技术

【研究成果】

【科研项目】

　　[1] 国家自然科学基金青年基金(61003079)， 2011.01-2013.12 　　[2] 陕西省科技攻关计划项目(2009K01-36)，2010.01-2011.12 　　[3] 教育部博士点基金(新教师计划)项目(20100203120012)，2011.01-2013.12 　　[4] 中央高校基本科研业务费资助项目(JY10000903014)， 2009.9-2011.9

【论文著作】

　　[1]. Haibin Zhang and Zhenhua Duan. Symbolic Algorithmic Analysis of Rectangular Hybrid Systems. Journal of Computer Science and Technology. 2009. 24(3): 531-543.(SCI: 000266386500011) 　　[2]. Haibin Zhang and Zhenhua Duan. Symbolic Algorithm Analysis of Hybrid Systems. Proceeding of The 5th Annual Conference on Theory and Applications of Models of Computation (TAMC’08). 2008. LNCS 4978. pp. 294-305. 　　[3]. Haibin Zhang and Zhenhua Duan. Model Checking Rectangular Hybrid Systems With Timed Computation Tree Logic. Proceeding of 4th IEEE International Symposium on Theoretical Aspects of Software Engineering. pp. 126-131. 2010. 　　[4]. Haibin Zhang and Zhenhua Duan. Symbolic Reachability Analysis of Rectangular Hybrid Systems. Proceeding of The 2th IEEE International Conference on Intelligent Computer Communication and Processing (ICCP’06). 2006. pp. 240-248. 　　[5]. Haibin Zhang and long Zhang. Synthesis of Hybrid Systems. Proceeding of IEEE International Conference on System Design and Data Proceesing. pp. 284-287, 2011. 　　[6]. Haibin Zhang, Weijun Zhun and long Zhang. Model Checking Hybrid Systems Within Hybrid Temporal Logic. Proceeding of IEEE International Conference on System Design and Data Proceesing. pp. 319-322, 2011. 　　[7]. Haibin Zhang, Xiaobing Wang, Liya Yang. Structures for Reachability Problems of Multirate Hybrid Systems. Proceeding of 3rd IEEE International Conference on Computer Design and Applications. accepted paper. 　　[8]. Haibin Zhang, Bohu Huang, Long Zhang. Model checking Multirate Hybrid Systems with Dense Timed Interval Temporal Logic. Proceeding of 3rd IEEE International Conference on Computer Design and Applications. accepted paper. 　　[9]. Weijun Zhu, Zhongyong Wang, Haibin Zhang. Intrusion Detection based on Model Checking Projection Temporal Logic, China Communications, 8(3): 66-72, 2011. 　　[10]. 张海宾，段振华. 混合系统的符号化可达性分析.软件学报.2008. 19(12): 3111-3121. 　　[11]. 朱维军, 张海宾, 周清雷. 离散时间区间时序逻辑可满足性的判定. 电子学报. 2010. 38(5): 1039-1045. 　　[12]. 张海宾，段振华. 稠密时间区间时序逻辑的可满足性判定. 西安电子科技大学学报. 2007. 34(3): 463-467. 　　[13]. 张海宾，段振华. 多速率混合系统的符号化可达性分析. 西安交通大学学报. 2007. 41(4): 412-415. 　　[14]. 张海宾，段振华. 多速率混合系统的模型检测. 西安电子科技大学学报. 2008. 35(1): 60-64. 　　[15]. 张海宾，段振华. 区间时序逻辑的模型检测. 西安电子科技大学学报. 2009. 36(2): 338-342. 　　[16]. 张海宾，段振华.混合投影时序逻辑与混合系统的形式化验证. 计算机科学. 2007. 34(11): 279-282. 　　[17]. 朱维军，张海宾，周清雷. 命题投影时序逻辑并发建模与自动验证，华中科技大学学报, 2010. 38(8): 77-80.