A sound abstract memory model for static analysis of C programs Online publication date: Wed, 16-May-2018
by Yukun Dong
International Journal of Computational Science and Engineering (IJCSE), Vol. 16, No. 3, 2018
Abstract: Abstract memory model plays an important role in the static analysis of programs. This paper proposes a region-based symbolic three-valued logic (RSTVL) to guarantee the soundness of static analysis, which utilises abstract regions to simulate blocks of the concrete memory. RSTVL applies symbolic expressions to express the value of memory objects, and the interval domain to describe the value of each symbol of symbolic expressions. Various operations for memory objects can be mapped to operations about regions. As a sound abstract memory model, RSTVL can describe the shape information of data structure in memory and the storage state of memory objects for C programs, and a variety of associative addressable expressions, including the point-to relations, hierarchical and valued logic relations. We have built a prototype tool DTSC_RSTVL that detects code level defects in C programs. Five popular C programs are analysed, the results indicate that the analysis is sufficiently sound to detect code level defects with zero false negative rate.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Computational Science and Engineering (IJCSE):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com
Our Blog 
Follow us on Twitter 
Visit us on Facebook