科研专业方向
研究领域:
基础软件
研究方向:
软件建模与分析、软件测试与验证
研究领域:
基础软件
研究方向:
软件建模与分析、软件测试与验证
合作单位 | 合作论文数量 |
---|---|
江苏省软件新技术与产业化协同创新中心 | 6 |
计算机软件新技术国家重点实验室 | 2 |
西北工业大学计算机学院 | 2 |
中国空间技术研究院 | 2 |
国防科学技术大学计算机学院并行与分布处理国防科技重点实验室 | 2 |
华东师范大学软件学院 | 2 |
北京大学信息科学技术学院软件研究所 | 2 |
高可信软件技术教育部重点实验室(北京大学) | 2 |
北京信息科技大学计算机学院 | 2 |
河海大学计算机与信息学院 | 2 |
南京晓庄学院数学与信息技术学院 | 2 |
南京中医药大学信息技术学院 | 2 |
新加坡国立大学计算学院计算机科学系 | 2 |
南京航空航天大学计算机科学与技术学院 | 2 |
中国科学技术大学计算机科学技术系 | 2 |
国防科技大学 | 1 |
中国科学院软件研究所 | 1 |
软件新技术国家重点实验室 | 1 |
澳门大学科技学院 | 1 |
中国科学院数学与系统科学研究院 | 1 |
计算机科学与技术系 | 1 |
南瑞集团公司(国网电力科学研究院) | 1 |
国电南瑞科技股份有限公司 | 1 |
论文标题 | 基金名称 |
---|---|
一种在静态类型面向对象语言中构造VFCG的方法 | 江苏省应用基础基金 |
面向方面的计算误差处理技术:实例研究与评估 | 国家自然科学基金 |
一种基于切片技术度量Java耦合性的框架 | 国家八六三高技术研究发展计划资助 |
程序理解研究与进展 | 江苏省应用基础 |
软件理解研究与进展 | 江苏省应用基础基金 |
检验实时系统的有序时段性质 | 国家自然科学基金 |
一种分析和理解程序的方法──程序切片 | 合肥经济技术学院科研基金项目编号99-183江苏省自然科学基金项目编号BK99038 |
C/C++程序静态内存泄漏警报自动确认方法 | 国家自然科学基金 |
BACH:线性混成系统有界可达性模型检验工具 | 国家自然科学基金 |
离散时段演算的符号模型验证 | 国家自然科学基金 |
基于MDE的异构模型转换:从MARTE模型到FIACRE模型 | 国家自然科学基金国家重点基础研究发展计划 |
面向基于场景规约的Web服务消息流分析与验证 | 国家自然科学基金项目 |
一种手绘制导的移动应用界面测试方法 | 国家重点研发计划 |
时间自动机可达性分析中的状态空间约减技术综述 | 国家自然科学基金 |
基于大数据的开源项目缺陷报告智能预检技术 | 国家重点研发计划基金资助项目 |
中断驱动系统模型检验? | 国家自然科学基金 |
中断驱动的嵌入式系统数据竞争检测工具 | 国家自然科学基金Nos.6132149161472179国家重点基础研究发展计划 |
一种基于MDA的UML顺序图到状态图的转换方法 | 国家自然科学基金 |
设计模式指导的软件分簇方法 | 国家自然科学基金 |
基于目标制导符号执行的静态缓冲区溢出警报自动确认技术 | 国家自然科学基金 |
LDPChecker——一个实时和混成系统模型检验工具 | 国家自然科学基金项目 |
常用循环摘要的自动生成方法及其应用 | 国家自然科学基金 |
UML实时活动图的形式化分析 | 国家自然科学基金 |
UML实时活动图的形式化分析 | 6 0 2 3 3 0 2 0 )国家八六三高技术研究发展计划基金 |
UML实时活动图的形式化分析 | 2 0 0 2AA1 1 6 0 90 )江苏省自然科学基金 |
一种手绘制导的移动应用界面测试方法 | 国家重点研发计划 |
场景驱动的构件行为抽取 | 国家自然科学基金国家重点基础研究发展规划基金 |
静动态结合的Java程序不变性分析方法 | 国家自然科学基金 |
基于迁移系统分析的线性混成系统安全验证 | 江苏省自然科学基金 |
一种动态消减时间自动机可达性搜索空间的方法 | 国家自然科学基金 |
基于污点分析的数组越界缺陷的静态检测方法 | 国家重点研发计划 |
基于目标制导符号执行的静态缓冲区溢出警报自动确认技术 | 国家自然科学基金 |
基于设计演算的形式化用例分析建模框架 | 国家自然科学基金国家重大基础研究发展计划 |
静动态结合的恶意Android应用自动检测技术 | 国家重点研发计划项目课题 |
基于应用视角的缓冲区溢出检测技术与工具 | 国家重点研发计划 |
基于状态机模型的构件健壮性测试 | 国家自然科学基金 |
一个面向路径的软件测试辅助工具 | 国家自然科学基金项目 |
软件开发方法发展回顾与展望 | 国家自然科学基金委-中国科学院学科发展战略研究项目:软件学科发展战略研究 |
基于MDA的设计模式建模与模型转换 | 国家自然科学基金国家重大基础研究发展计划 |
基于分类树的随机测试用例生成 | 国家自然科学基金 |
面向对象的类型-子类型分析及推理规则 | 江苏省应用基础 |
面向模型检验的UML状态机语义 | 8 63项目 |
模型层次与自省思想研究 | 国家重点自然基金项目 |
线性混成系统的参数分析 | 国家自然科学基金国家八六三高技术研究发展计划 |
线性混合系统的一种验证方法 | 国家‘863’高科技项目基金 |
基于博弈论的开放环境下场景规约监控语义 | 国家自然科学基金 |
一种系统依赖图的面向对象扩充方案 | 国家863青年基金资助项目 |
基于随机时间自动机和统计模型检验技术的无线传感网络协议建模与分析 | 国家自然科学基金 |
一种基于结构查询的UML设计模式识别方法 | 国家自然科学基金 |
基于约束求解的代码查询技术在StackOverflow上的实证研究 | 国家自然科学基金 |
SDT:一个面向场景规约的运行时测试工具 | 本文的研究工作受到国家自然科学基金 |
面向WebServices的模型驱动开发方法 | 国家自然科学基金 |
UML时间顺序图的可达性分析 | 国家自然科学基金 |
UML模型到COOZ规约的形式化转换 | 国家自然科学基金资助 |
程序数值误差的扰动检测与优化 | 国家自然科学基金 |
接口自动机——一种用于组件组合的形式系统 | 国家自然科学基金编号:60273036国家重大基础研究计划973项目编号:2002CB312001江苏省自然科学基金编号:BK2004080 |
基于MDA的UML模型转换:从功能模型到实现模型 | 国家重点自然基金 |
基于MDA的UML模型转换:从功能模型到实现模型 | 江苏省自然基金 |
基于数据切片度量JAVA内聚性 | 国家 8 6 3青年基金资助项目 |
基于组合IIS路径抽取的组合线性混成系统有界可达性分析优化 | 国家重点基础研究发展计划 |
随机模型检验研究 | 国家自然科学基金项目 |
一种面向对象程序的分层切片方法 | 国家 8 6 3青年基金资助项目 |
嵌入式软件建模、实现与验证:研究与进展 | 国家自然科学基金 |
获2002年教育部自然科学二等奖、
1998年教育部科学技术进步二等奖
1998年度中创软件人才奖,
获国务院政府特殊津贴,
入选教育部跨世纪人才培养计划和江苏省青蓝工程学术带头人培养计划,
2002年被教育部表彰为高等学校优秀骨干教师,
2004年获国家杰出青年科学基金资助。
迎接人机物融合泛在计算时代,提升关键软件技术创新与供给能力
基于大数据的开源项目缺陷报告智能预检技术
基于大数据的开源项目缺陷报告智能预检技术
一种手绘制导的移动应用界面测试方法
基于污点分析的数组越界缺陷的静态检测方法
软件开发方法发展回顾与展望
基于应用视角的缓冲区溢出检测技术与工具
基于应用视角的缓冲区溢出检测技术与工具
基于约束求解的代码查询技术在StackOverflow上的实证研究
面向事件驱动智能家居物联网系统的自动化配置、仿真与验证平台
软件开发方法发展回顾与展望
C/C++程序静态内存泄漏警报自动确认方法
常用循环摘要的自动生成方法及其应用
C/C++程序静态内存泄漏警报自动确认方法
常用循环摘要的自动生成方法及其应用
静动态结合的恶意Android应用自动检测技术
静动态结合的恶意Android应用自动检测技术
基于组合IIS路径抽取的组合线性混成系统有界可达性分析优化
基于组合IIS路径抽取的组合线性混成系统有界可达性分析优化
一种符号执行制导的循环内界分析方法
基于目标制导符号执行的静态缓冲区溢出警报自动确认技术
基于目标制导符号执行的静态缓冲区溢出警报自动确认技术
中断驱动系统模型检验?
中断驱动的嵌入式系统数据竞争检测工具
中断驱动的嵌入式系统数据竞争检测工具
中断驱动系统模型检验?
随机模型检验研究
随机模型检验研究
一种面向信息物理融合系统安全攸关场景的测试用例自动生成方法
设计模式指导的软件分簇方法
设计模式指导的软件分簇方法
基于博弈论的开放环境下场景规约监控语义
一种基于结构查询的UML设计模式识别方法
程序数值误差的扰动检测与优化
一种基于结构查询的UML设计模式识别方法
基于博弈论的开放环境下场景规约监控语义
程序数值误差的扰动检测与优化
基于迁移系统分析的线性混成系统安全验证
面向维护的实时软件时间变化敏感点检测
基于随机时间自动机和统计模型检验技术的无线传感网络协议建模与分析
基于迁移系统分析的线性混成系统安全验证
面向方面的计算误差处理技术:实例研究与评估
面向方面的计算误差处理技术:实例研究与评估
BACH:线性混成系统有界可达性模型检验工具
形式化方法与工具专刊前言
一种目标制导的混合执行测试方法
以偶然正确性概率为基础的测试充分度准则
BACH:线性混成系统有界可达性模型检验工具
形式化方法与工具专刊前言
静动态结合的Java程序不变性分析方法
内存泄漏检测工具与评估方法
死锁检测工具的能力分析与综合应用
基于状态机模型的构件健壮性测试
基于状态机模型的构件健壮性测试
基于MDE的异构模型转换:从MARTE模型到FIACRE模型
面向基于场景规约的Web服务消息流分析与验证
基于MDE的异构模型转换:从MARTE模型到FIACRE模型
基于分类树的随机测试用例生成
基于认识与理解途径的软件可信性度量与评估
Internet环境下基于构件的软件理论与方法专刊前言
基于设计演算的形式化用例分析建模框架
基于设计演算的形式化用例分析建模框架
基于MDA的设计模式建模与模型转换
场景驱动的构件行为抽取
一种动态消减时间自动机可达性搜索空间的方法
J2EE平台上的所见即所得的HTML电子表格工具的设计
面向服务的计算专刊前言
UML行为图驱动的Java程序运行时验证工具
时间自动机可达性分析中的状态空间约减技术综述
从EDOC的业务过程建模到J2EE应用程序框架的MDA转换
基于场景规约的构件式系统设计分析与验证
SDT:一个面向场景规约的运行时测试工具
面向WebServices的模型驱动开发方法
LDPChecker——一个实时和混成系统模型检验工具
实时系统的模型检验中针对共享变量的优化技术
J2EE平台上的HTML电子表格工具的设计
模型驱动的软件测试研究
面向设计流图的代码支撑工具
从ExecutableUML模型到J2ME程序
一种基于J2EE平台的MDA模型转换技术
基于MDA的PIM到J2EE平台PSM的转换方法
ME4ET:一个基于EDOCER模型的模型转换工具
QRDChecker:一个QRDC模型检验工具
模型层次与自省思想研究
模型层次与自省思想研究
UML时间顺序图的可达性分析
接口自动机——一种用于组件组合的形式系统
基于MDA的UML模型转换:从功能模型到实现模型
嵌入式软件建模、实现与验证:研究与进展
一个MDA支撑工具的设计与实现
一种基于MDA的UML顺序图到状态图的转换方法
UML实时活动图的形式化分析
一个基于UML协作图的集成测试用例生成方法
基于MDA的UML模型转换技术——从顺序图到状态图
基于UML顺序图的测试方法
一个基于UML顺序图的场景测试用例生成方法
一个面向路径的软件测试辅助工具
MDA的设想与实现
检验实时系统的有序时段性质
基于J2EE平台的MDA模型转换技术
基于认识与理解途径的软件可信性度量与评估体系及支撑技术研究
网构化软件关键技术、平台与应用
软件工程中的形式化方法和面向对象技术研究
一种基于硬件的程序动态函数调用序列追踪方法和装置
一种基于符号执行的栈操作二进制代码优化方法和装置
一种基于硬件的高级程序动态控制流追踪方法和装置
一种基于图计算的代码分析的方法和装置
一种经验库制导的浮点程序优化加速方法
神经网络分类识别中的对抗样本生成的方法和装置
一种基于共享不可行路径池的代码并行验证方法和装置
一种智能家居物联网系统受攻击安全验证的方法和装置
一种智能家居物联网系统受攻击安全验证的方法和装置
一种智能家居线性时序逻辑规约生成的方法和装置
一种用于人工智能数据分析的大数据高保真可视化方法
一种用于大规模系统中状态相关缺陷的静态检测方法
基于GPU的大规模软件高精度静态分析方法
一种面向偏好设置的安卓应用测试方法
一种基于字节码操作的安卓软件增强测试方法
一种基于中断序列图的中断驱动系统验证方法
一种基于强化学习的Android应用自动测试方法及系统
一种分析组合线性混成自动机全局可达的方法和装置
一种基于黑盒函数与机器学习的代码测试生成方法和装置
一种基于目标规约满足度评估的并发程序合成方法和装置
一种基于插桩的针对Android系统动态加载情况的隐私保护方法
一种数值程序的全局优化方法
一种基于深度学习与程序合成的C/C++程序缺陷自动修复方法
一种基于机器学习的C程序内存泄漏智能化检测方法
一种将程序代码转换成数据约束的方法和装置
基于模型转换由midcore生成Spark和Hadoop程序代码的方法
一种基于模型转换的从iOS到Android的跨平台页面转化方法
一种基于词向量的多平台控件对应方法
一种基于IFML的iOS开发建模方法
一种基于模型变更的自动维护测试脚本的方法
基于XACML访问控制机制的Android应用访问控制代码生成方法
一种基于程序合成的C/C++程序缺陷自动修复方法
一种静动态结合的恶意安卓应用自动检测系统
一种自动合成常用循环的摘要并生成程序规约的方法
一种面向线性约束代码的有界可达性验证方法
一种智能家居物联网系统验证与修复的方法和装置
一种基于API文档的约束自动生成方法
一种基于IFML的Android开发建模方法
一种由转换原语生成Spark代码的方法
基于手绘识别的图形界面测试用例生成方法
一种基于扩展的IFML的移动应用的测试用例生成方法
一种基于扩展的UML2序列图的中断驱动系统建模方法
一种基于代码变更的移动应用测试脚本自动维护方法
一种基于代码变更的移动应用测试脚本自动维护方法
一种针对异常处理代码的测试方法
缓冲区溢出漏洞自动修复方法
一种多触发机制CPS在线建模与检验的方法和装置
一种多触发机制CPS在线建模与检验的方法和装置
一种基于约束求解的智能电网系统鲁棒性验证方法
一种基于约束求解的智能电网系统鲁棒性验证方法
一种基于MongoDB实现图转换的方法和装置
一种基于MongoDB实现图转换的方法和装置
基于机器学习的自适应网络爬虫方法
基于符号执行路径剪枝的缓冲区溢出漏洞自动检测方法
基于符号执行路径剪枝的缓冲区溢出漏洞自动检测方法
一种将源代码存入图数据库的方法
一种基于逆向工程的模型库构造方法
一种基于MongoDB的云端代码查询方法与装置
一种基于MongoDB的云端代码查询方法与装置
基于路径片段频谱的符号执行搜索方法
基于路径片段频谱的符号执行搜索方法
一种递归最大执行频度与深度的静态估计方法
一种递归最大执行频度与深度的静态估计方法
一种实时系统的循环边界内向分析方法
一种实时系统的循环边界内向分析方法
动静态结合的中断驱动程序数据竞争检测方法
动静态结合的中断驱动程序数据竞争检测方法
基于抽象解释的线性混成系统不变式的生成方法
基于抽象解释的线性混成系统不变式的生成方法
基于统计模型检验的不稳定网络鲁棒性评测方法
基于增量线性规划的动态系统在线增量式快速验证系统及方法
基于增量线性规划的动态系统在线增量式快速验证系统及方法
一类非线性混成系统的建模与面向路径的可达性分析方法
面向线性混成系统的等价迁移系统构造方法
面向线性混成系统的等价迁移系统构造方法
一种基于类属性指导的UML模型查询方法
设计模式制导的爪哇代码评审方法
设计模式制导的爪哇代码评审方法
一种基于活动图模型的系统行为仿真方法
一种基于活动图模型的系统行为仿真方法
一种智能手机遥控智能电视的交互方法
一种智能手机遥控智能电视的交互方法
一种智能手机应用交互界面程序可用性测试方法
一种智能手机应用交互界面程序可用性测试方法
一种基于测试的静态分析误报消除方法
基于代码生成和符号执行的访问控制策略测试自动生成方法
基于代码生成和符号执行的访问控制策略测试自动生成方法
一种基于代码变更的软件模型同步方法
一种基于代码变更的软件模型同步方法
最小不满足树制导的混成系统可达性分析方法
一种混成系统的可达性分析方法
最小不满足树制导的混成系统可达性分析方法
一种基于模型检验的无线传感器网络安全协议验证方法
一种基于模型检验的无线传感器网络安全协议验证方法
一种控制器局域网帧传输验证方法
一种基于动态树的无线传感网目标跟踪方法
一种基于动态树的无线传感网目标跟踪方法
一种移动无线传感器网络分布式目标跟踪方法
基于源代码查询的半自动插桩方法
一种基于MARTE建模语言和Theme方法的嵌入式系统建模方法