支持形状分析的符号执行引擎的设计与实现

• 作者: 朱玲 李兆鹏 梁家彪 沈咸飞
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 符号执行 静态分析 循环不变式 递归函数
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 193-198
• 页数: 6页
• 分类号: TP311
• 字数: 7386字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2016.3.036

摘要

目前提高软件可靠性的方法有3种:动态测试、静态分析和程序验证.动态测试的结果依赖于测试集的设计,误报率低,漏报率高,分析结果不稳定.程序验证可以对程序的各种性质进行完备的验证.但目前程序验证通常都需要手动证明,分析成本最高.而程序静态分析可以更早、更全面、较高效和低成本地检测到程序中的缺陷.其中符号执行技术是一种比较有应用前景的静态分析技术,可以很好地控制精确度.针对符号执行可伸缩性差和容易产生路径爆炸的问题,在符号执行过程中利用形状分析技术实现自动推导循环不变式和构建函数行为规范,实现了一个较为实用的C程序分析工具.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	朱玲	中国科学技术大学计算机科学与技术学院	29	126	7.0	9.0
2	梁家彪	中国科学技术大学计算机科学与技术学院	2	12	2.0	2.0