A Low-Level Memory Model and an Accompanying Reachability Predicate

Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric. International Journal on Software Tools for Technology Transfer (STTT), 2009. (Invited.)
[pdf] [bib]

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.

Bibtex:

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