个人简历

金大海
所属中心 服务基础研究中心
职称 副教授
承担课程《软件可靠性》
个人介绍
北京邮电大学副教授，硕士生导师。2006年毕业于解放军装甲兵工程学院，工学博士学位，2008年进入北京邮电大学博士流动站，现任职于北京邮电大学网络技术研究院。中国计算机学会会员，计算机学会容错计算专业委员会委员，主要从事软件静态分析及测试的相关理论研究工作。在《计算机学报》、《软件学报》、《计算机研究与发展》等国内顶级期刊及ATS、QSIC、APSEC、IWPD等测试相关国际会议上发表论文50余篇。负责研发的软件缺陷检测系统——DTS在全国有500 多用户，遍布于航天、航空、武器、金融、交通等高可信领域，在嫦娥、天宫和探月工程中得到较好的应用，取得了较好的经济效益和社会效益。研究成果申请国家发明专利近三十项（授权七项），申请软件著作权十余项，编写软件测试专著一本。

承担课题
1．总参第五十四研究所专项研究项目，***，2014/10-2015/10，92万元，在研，主持。
2．国家自然科学基金重大研究计划集成项目，91318301，“可信软件理论、方法集成与综合试验平台”子课题，2013/06-2016/12，50万元，在研，主持。
3．网络与交换技术国家重点实验室探索类项目，基于DTS的缺陷检测结果自动化关联技术研究，2013/07-2015/07，10万元，在研，主持。
4．国家高技术研究发展计划（863计划），2012AA011201，“网构化软件协同生产和运行演化集成平台及服务环境”子课题，2012/01-2014/12，100万元，已结题，主持。
5．上海证劵交易所联合研究计划项目，证券业关键业务系统代码质量保证检查方法与工具研究，2012/06-2013/06，10万元，已结题，主持。
6．北京邮电大学青年科研创新计划专项课题，代码缺陷检测技术中的缺陷模式自定制方法研究，2012/01-2014/12，12万元，已结题，主持。
7．网络与交换技术国家重点实验室探索类项目，空指针引用充分性检测技术研究，2012/10-2013/11，10万元，已结题，主持。
8．网络与交换技术国家重点实验室探索类项目，提高代码缺陷检测精度的技术研究，2011/06-2012/08，10万元，已结题，主持。
9．国家自然科学基金重大研究计划培育项目，91018002、航天嵌入式软件缺陷检测方法研究、系统研发及应用，2011/01-2011/12，50万元，已结题，参与。
10．国家高技术研究发展计划（863计划），2009AA01Z404 ，软件的安全性缺陷模式及基于安全性缺陷模式的测试技术，2009/01-2010/12，85万元，已结题，参与。
11．国家高技术研究发展计划（863计划），2007AA010302 ，“支持软件可信性分析和评估的生产线”子课题，2007/10-2010/12，100万元，已结题，参与。
12．国家高技术研究发展计划（863计划），2006AA01Z184，软件的故障模型与面向故障的软件测试系统，2006/12-2008/10，91万元，已结题，参与。

获奖和成果
专利
(1) 金大海,宫云战,黄俊飞,王雅文,张大林,一种基于抽象解释技术的缺陷警报 分组方法及装置,2014.3.26-2033.12.13,北京,CN201310687844.3。
(2) 金大海,宫云战,董玉坤,王雅文,黄俊飞,一种充分检测空指针引用缺陷的方 法,2013.7.24-2033.4.22,北京,CN201310141769.0。
(3) 金大海,宫云战,张大林,黄俊飞,王雅文,一种缺陷关联方法及装置,2013.6. 26-2033.4.12,北京,CN201310128097.X。
(4) 金大海,张大林,宫云战,王雅文,黄俊飞,一种基于状态分区的静态缺陷检测 求精方法,2014.7.16-2034.4.8,北京,CN201410138438.6。
(5) 金大海,王前,宫云战,黄俊飞,王雅文,生成时序安全属性类缺陷模式相关的 函数摘要信息的方法,2014.7.9-2034.3.25,北京,CN201410115283.4。
(6) 金大海,宫云战,赵云山,肖庆,王思岚,循环语句中变量抽象取值的迭代求精 方法,2012.6.13-2031.12.5,北京,CN201110400173.9。
(7) 金大海,宫云战,周虹伯,王雅文,黄俊飞,赵云山,王前,一种基于别名分析 技术的软件测试方法,2011.4.20-2030.12.28,北京,CN201010622568.9。
(8) 金大海,宫云战,杨朝红,肖庆,黄俊飞,王雅文,应用异常控制流集的软件测 试方法及系统,2010.9.29-2030.6.1,北京,CN201010188376.1。

研究领域

软件静态分析与缺陷检测

近期论文

(1) 金大海，宫云战，杨朝红，肖庆，运行时异常对软件静态测试的影响研究，计算机学报，2011，第6期：1090~1099
(2) 金大海，宫云战，杨朝红，肖庆，过程约束信息在软件静态测试中的应用，计算机辅助设计与图形学学报，2011，第3期：534~542
(3) 金大海，宫云战，杨朝红，肖庆，函数后置信息在软件静态测试中的应用，北京邮电大学学报，2010，第33卷，第6期，103~107
(4) 董玉坤，金大海，宫云战，邢颖，基于区域内存模型的C程序静态分析，软件学报，2014，25(2)：357~372
(5) 张大林，金大海，宫云战，王前，董玉坤，张海龙，基于缺陷关联的静态分析优化，软件学报，2014，25(2)：368~399
(6) 张大林，金大海，宫云战，张海龙，杨学红，基于踪迹挖掘的自动缺陷警报分类方法，中国科学，2014，44(1)：91~107
(7) 董玉坤，宫云战，金大海，基于区域内存模型的空指针引用缺陷检测，电子学报，2014，42(9)：1744~1752
(8) 周虹伯，金大海，宫云战，基于域敏感指向分析的区间运算在软件测试中的应用，计算机研究与发展，2012， 49(9)：1852~1862
(9) 刘莉，金大海，宫云战，提高区间运算的循环处理精度，清华大学学报(自然科学版), 2011，第S1期：1483~1486
(10) 杨睿，金大海，宫云战，马跃，Java中空指针引用故障的静态检测方法，清华大学学报(自然科学版)，2011，第S1期：1509~1514
(11) 肖庆，宫云战，杨朝红，金大海，王雅文，一种路径敏感的静态缺陷检测方法，软件学报，2010，21(2)：209~217
(12) Zhou Hongbo，Wang Qian，Jin Dahai，Gong Yunzhan，A Static Detecting Model for Invalid Arithmetic Operation Based on Alias Analysis，IWPD2012, Dallas, 2012.11.27-11.30
(13) Zhou Hongbo，Jin Dahai，Gong Yunzhan，An interval-based model for detecting software defect using alias analysis，APSEC2012, Hong Kong, 2012.12.4-12.7