Abstract

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.

Citation

Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric
A Low-Level Memory Model and an Accompanying Reachability Predicate
International Journal on Software Tools for Technology Transfer (STTT), 11(2): 105-116, 2009.

BibTeX

@article{2009_sttt_clqr,
  title = {A Low-Level Memory Model and an Accompanying Reachability Predicate},
  author = {Shaunak Chatterjee and Shuvendu Lahiri and Shaz Qadeer and Zvonimir Rakamaric},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  publisher = {Springer},
  volume = {11},
  number = {2},
  pages = {105-116},
  month = {February},
  year = {2009}
}

Abstract

Citation

BibTeX

Resources