Concrete Memory Models for Shape Analysis

This paper discusses four store-based concrete memory models. We characterize memory models by the class of pointers they support and whether they use numerical or symbolic offsets to address values in a block. We give the semantics of a C-like language within each of these memory models to illustrate their differences. The language we consider is a fragment of Leroy's Clight, including arrays, pointer arithmetics but excluding casts. All along the paper, we link these concrete memory models with existing shape analyses.

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: Pascal Sotin, Bertrand Jeannet, Xavier Rival
• Keywords: Concrete Memory Models, ENTCS 2010, Memory Models, Software Engineering, Store-based Concrete Memory