ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2016, Vol. 53 ›› Issue (1): 155-164.doi: 10.7544/issn1000-1239.2016.20150669

所属专题: 2016优青专题

• 软件技术 • 上一篇    下一篇

基于CEGAR的C程序空指针解引用检测

段钊,田聪,段振华   

  1. (西安电子科技大学计算机理论与技术研究所 西安 710071) (ctian@mail.xidian.edu.cn)
  • 出版日期: 2016-01-01
  • 基金资助: 
    国家自然科学基金项目(61322202,61420106004,91418201,61133001,61272117)

CEGAR Based Null-Pointer Dereference Checking in C Programs

Duan Zhao, Tian Cong, Duan Zhenhua   

  1. (Institute of Computing Theory and Technology, Xidian University, Xi’an 710071)
  • Online: 2016-01-01

摘要: 随着计算机软件规模和复杂度的日益增长,软件系统的可靠性和安全性倍受关注.空指针解引用是程序中常见的一类错误.提出了一种基于反例制导抽象精化CEGAR的C程序空指针解引用检测方法.该方法首先使用线性时序逻辑描述空指针解引用问题,然后通过抽象精化的方法检测待测程序中是否含有空指针解引用错误.为了达到完全自动验证的目标,同时针对空指针解引用问题,研究了该类性质的时序逻辑表达方法,并自动从程序中针对所有的指针变量,形成相应的时序逻辑公式.实验结果表明,所提出的方法在大规模C程序的空指针解引用检测方面有着重要的实际应用价值.

关键词: 模型检测, 抽象精化, 空指针解引用, 程序验证, 时序逻辑

Abstract: With the rapid growth of computer software in both scale and complexity, more and more attention has been paid by software developers on the reliability and security issue. Null-pointer dereference is a kind of errors which often occur in programs.This paper proposes a CEGAR based null-pointer dereference verification approach for C programs. With this method, first, a linear temporal logic (LTL) formula is used to specify the null-pointer dereference problem. Then whether null-pointer dereference occuring in a program is checked by a CEGAR based model checking approach. In order to verify null-pointer dereference problem in a total automatic way, this paper also studies how to generate temporal logic formulas automatically with respective to null-pointer dereference problem. Experimental results show that the proposed approach is useful in practice for checking null-pointer dereference in C programs with large scale.

Key words: model checking, abstraction refinement, null-pointer dereference, program verification, temporal logic

中图分类号: