CEGAR Based Null-Pointer Dereference Checking in C Programs

Duan Zhao; Tian Cong; Duan Zhenhua

doi:10.7544/issn1000-1239.2016.20150669

Journal of Computer Research and Development > 2016 > 53(1): 155-164. > DOI: 10.7544/issn1000-1239.2016.20150669 CSTR: 32373.14.issn1000-1239.2016.20150669

Duan Zhao, Tian Cong, Duan Zhenhua. CEGAR Based Null-Pointer Dereference Checking in C Programs[J]. Journal of Computer Research and Development, 2016, 53(1): 155-164. DOI: 10.7544/issn1000-1239.2016.20150669

Citation:

PDF (2121 KB)

CEGAR Based Null-Pointer Dereference Checking in C Programs

(Institute of Computing Theory and Technology, Xidian University, Xi’an 710071)

More Information

Published Date: December 31, 2015

Graphical Abstract

Abstract

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.
- model checking,
- abstraction refinement,
- null-pointer dereference,
- program verification,
- temporal logic

FullText(HTML)

References (0)

[1]	Li Xinran, Li Rongshou, Qin Chuan, Qian Zhenxing, Zhang Xinpeng. Generative Information Hiding Method Based on Couplet Carrier[J]. Journal of Computer Research and Development, 2025, 62(3): 779-789. DOI: 10.7544/issn1000-1239.202330663
[2]	Wang Shuo, Wang Jianhua, Tang Guangming, Pei Qingqi, Zhang Yuchen, Liu Xiaohu. Intelligent and Efficient Method for Optimal Penetration Path Generation[J]. Journal of Computer Research and Development, 2019, 56(5): 929-941. DOI: 10.7544/issn1000-1239.2019.20190012
[3]	He Yanxiang, Chen Yong, Wu Wei, Xu Chao, Li Qingan. Bus-Invert Encoding Oriented Low Power Scheduling Method[J]. Journal of Computer Research and Development, 2014, 51(8): 1773-1780. DOI: 10.7544/issn1000-1239.2014.20130066
[4]	Wang Changjing, Luo Haimei, Zuo Zhengkang. Formal Software Specification Generation Approach Based on Problem Patterns[J]. Journal of Computer Research and Development, 2013, 50(2): 352-360.
[5]	Wang Weizheng, Kuang Jishun, You Zhiqiang, Liu Peng. A Low-Power and Low-Cost BIST Scheme Based on Capture in Turn of Sub-Scan Chains[J]. Journal of Computer Research and Development, 2012, 49(4): 864-872.
[6]	Luo Zuying, Pan Yuedou. Transistor-Level Methodology on Power Optimization for CMOS Circuits[J]. Journal of Computer Research and Development, 2008, 45(4): 734-740.
[7]	Zhou Hongwei, Zhang Chengyi, and Zhang Minxuan. A Method of Statistics-Based Cache Leakage Power Estimation[J]. Journal of Computer Research and Development, 2008, 45(2): 367-374.
[8]	Wen Dongxin, Yang Xiaozong, and Wang Ling. A High Level Synthesis Scheme and Its Realization for Low Power Design in VLSI[J]. Journal of Computer Research and Development, 2007, 44(7): 1259-1264.
[9]	Ma Zhiqiang, Ji Zhenzhou, and Hu Mingzeng. A Low Power Data Cache Design Based on Very Narrow-Width Value[J]. Journal of Computer Research and Development, 2007, 44(5): 775-781.
[10]	Ma Zhiqiang, Ji Zhenzhou, and Hu Mingzeng. A Low-Power Instruction Cache Design Based on Record Buffer[J]. Journal of Computer Research and Development, 2006, 43(4): 744-751.