English 
黄志球

教授

招生学科专业:
计算机科学与技术 -- 【招收博士、硕士研究生】 -- 计算机科学与技术学院
软件工程 -- 【招收博士、硕士研究生】 -- 计算机科学与技术学院
网络空间安全 -- 【招收博士、硕士研究生】 -- 计算机科学与技术学院
电子信息 -- 【招收博士、硕士研究生】 -- 计算机科学与技术学院

毕业院校:南京航空航天大学

学历:南京航空航天大学

学位:工学博士学位

所在单位:计算机科学与技术学院/人工智能学院/软件学院

联系方式:025-84892400

电子邮箱:

手机版

访问量:

最后更新时间:..

当前位置: 主页 >> 科学研究 >> 论文成果
支持抽象解释的静态分析方法的形式化体系研究

点击次数:

所属单位:计算机科学与技术学院/人工智能学院/软件学院

发表刊物:计算机科学

关键字:形式化方法;静态分析;抽象解释;可配置程序分析;

摘要:在安全关键领域中,如何保证软件的安全性已经成为了一个广受关注的重要课题。静态程序分析是一类十分有效的程序自动化验证方法。基于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出。可配置程序分析(Configurable Program Analysis,CPA)是一种通用静态分析方法形式化体系,旨在用一种形式化体系对静态分析的分析阶段进行建模。使用CPA对基于抽象解释的静态分析进行建模,给出如何使用CPA形式化体系描述基于抽象解释的静态分析,给出了从待分析程序到CPA形式化体系的转换规则;提供了一种在安全关键性领域中的软件正确性自动验证方法,为基于抽象解释的静态分析工具的实现提供了一种可行方案。

是否译文:

发表时间:2017-12-15

合写作者:张弛,丁泽文

通讯作者:黄志球

版权所有©2018- 南京航空航天大学·信息化处(信息化技术中心)