STVL: Improve the Precision of Static Defect Detection with Symbolic Three-Valued Logic

Among various abstract domains, the interval domain is simple but also less precise. To improve the precision of static defect detection based on the interval domain, we propose a symbolic three-valued logic (STVL) based interval analysis. Our STVL differs from other symbolic techniques in that it i...

Full description

Saved in:
Bibliographic Details
Main Authors: Yunshan Zhao, Yawen Wang, Yunzhan Gong, Honghe Chen, Qing Xiao, Zhaohong Yang
Format: Conference Proceeding
Language:English
Subjects:
Analytical models
Concrete
Context
Context modeling
Data structures
inter/intra-procedural analysis
interval analysis
pointer analysis
Polynomials
procedure summary
Reactive power
symbolic execution
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Among various abstract domains, the interval domain is simple but also less precise. To improve the precision of static defect detection based on the interval domain, we propose a symbolic three-valued logic (STVL) based interval analysis. Our STVL differs from other symbolic techniques in that it is capable of handling the logical relationship between variables, which could help eliminating false positives. In addition, for the pointer related defect detection, we introduce a STVL-based pointer model, which naturally supports the pointer arithmetic operation, alias analysis and point-to memory abstraction. Moreover, we present a unified symbolic procedure summary model, also STVL-based, to extract the call effect of each invocation and achieve context-sensitivity. Experimental results indicate that the technique is able to achieve sizable precision improvements at reasonable costs, compared with the none-symbolic method.
ISSN:1530-1362
2640-0715
DOI:10.1109/APSEC.2011.23