A low-level memory model and an accompanying reachability predicate

Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer m...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2009-04, Vol.11 (2), p.105-116
Main Authors: Chatterjee, Shaunak, Lahiri, Shuvendu K., Qadeer, Shaz, Rakamarić, Zvonimir
Format: Article
Language:English
Subjects:
Computer memory
Computer Science
Information processing
Software Engineering
Software Engineering/Programming and Operating Systems
Special Section on TACAS07
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software. The reachability predicate has already proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. In this paper, we present a memory model suitable for reasoning about low-level pointer operations that is accompanied by a formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present our experience with a prototype verifier on a set of illustrative C benchmarks.
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-009-0098-1