可信软件分析与验证技术

可信软件分析与验证技术是提升软件质量的关键途径，国内首次提出了恶意软件检测新方法，给出了并发程序的时序一致性模型，在能量感知评估和软件正确性验证技术方面取得了创新性成果。

软件非功能性验证：

1. 针对大规模并发程序的时序一致性问题，提出了基于系统吞吐量的时序一致性模型；

2. 给出了时序约束设置与检测点选择方法，以及时序一致性验证技术；

解决了传统大规模并发程序时序一致性验证时面临的效率低下问题

软件安全性验证：

1. 针对恶意软件检测领域，提出了基于下推自动机的可执行软件分析方法，弥补了已有方法无法模拟软件运行栈的问题。

设计了基于模型检测的恶意代码检测方法，开发了原型工具，克服了静态分析不能识别未知恶意代码和动态分析不能全覆盖的缺陷，有效地提高了恶意代码检测的正确率。

能量感知评估验证技术：

1. 基于统计模型检测技术评估、预测智能建筑的能耗，并借助统计模型验证器定量分析系统的能耗，以预测系统的电能使用情况。

成果已被应用于丹麦**部的建筑管理部门，并形成相关标准，对整个系统所需要的电量进行预测与评估

软件功能性验证：

1. 设计了一种新颖的基于线性时态逻辑的可满足性判断算法，该算法在同类技术中综合性能最优。

提出了用于复杂系统量化建模的形式化技术，为验证软件量化性质提供了分析基础和技术保障。

成果：

1. 在领域重要期刊和会议共发表文章50多篇，获得国际同行的广泛关注与高度认可。

部分成果获第三届杨嘉墀科技奖二等奖