ISCAS OpenIR  > 基础软件与系统重点实验室
C程序的静态分析
许中兴
Major计算机软件与理论
Supervisor张健
2009-06-05
Degree Grantor中国科学院研究生院
Degree Level博士
Place of Degree Grantor北京
Keyword程序分析,bug查找,编译器
English Abstract

近年来,随着软件在社会生活中的作用越来越重要,软件的正确性也越来越受到人们的重 视。然而如何保证软件的正确性却是一个一直都没有得到很好解决的问题。在上世纪六七 十年代人们就提出了程序验证的概念,但是程序验证一直不能很好的处理用实用的程序设 计语言编写的程序,并且自动化程度也不高,现代软件的规模往往有数百万行代码,导致 程序验证无法得以应用。另一方面,面向大规模实际程序的传统数据流分析主要的应用是 编译优化,它们的目标是获取保守的、粗略的程序信息,从而也不适合于程序正确性的检 测。 随着计算性能的提高以及自动定理证明技术的成熟,另一大类基于符号执行的精确的程序 分析技术逐渐被人们所重视。符号执行是一种假设输入变量为符号值,精确的模拟程序执 行的路径敏感的静态分析方法。符号执行在上世纪七十年代被提出,但是由于无法处理程 序中的指针、数组等语言成分,一直无法得以广泛应用。本文针对使用极为广泛的C语言, 设计了一套完整精确模拟C 语言语义的算法和技术,包括内存建模,对各种表达式语义的 模拟,函数调用的处理等。 作为符号执行技术的两种应用,本文对自动测试数据生成和内存泄漏检测分别进行了研究, 提出了完整的算法,并实现了相应的工具。本文描述的符号执行算法目前已经在开源编译 器Clang中得以实现,并还在不断改进之中。

Language中文
Content Type学位论文
URIhttp://ir.iscas.ac.cn/handle/311060/92
Collection基础软件与系统重点实验室
Recommended Citation
GB/T 7714
许中兴. C程序的静态分析[D]. 北京. 中国科学院研究生院,2009.
Files in This Item:
File Name/Size DocType Version Access License
thesis.pdf(906KB)学位论文 开放获取CC BY-NC-SAApplication Full Text
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[许中兴]'s Articles
Baidu academic
Similar articles in Baidu academic
[许中兴]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[许中兴]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.
 

Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.