Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1016/j.entcs.2010.09.012 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
symbolic offset,memory model,c-like orogramming languages,c-like language,concrete memory model,shape analysis,concrete memory models,language semantics,pointer arithmetics,store-based concrete memory model,memory models | Pointer (computer programming),Programming language,Placement syntax,Language semantics,Computer science,Theoretical computer science,Memory map,Semantics,Shape analysis (digital geometry) | Journal |
Volume | Issue | ISSN |
267 | 1 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
2 | 0.36 | 7 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Pascal Sotin | 1 | 32 | 3.38 |
Bertrand Jeannet | 2 | 641 | 29.06 |
Xavier Rival | 3 | 571 | 32.33 |