A Scalable Memory Model for Low-Level Code

Abstract. Because of its critical importance underlying all other software, lowlevel system software is among the most important targets for formal verification. Low-level systems software must sometimes make type-unsafe memory accesses, but because of the vast size of available heap memory in today’s computer systems, faithfully representing each memory allocation and access does not scale when analyzing large programs. Instead, verification tools rely on abstract memory models to represent the program heap. This paper reports on two related investigations to develop an accurate (i.e., providing a useful level of soundness and precision) and scalable memory model: First, we compare a recently introduced memory model, specifically designed to more accurately model low-level memory accesses in systems code, to an older, widely adopted memory model. Unfortunately, we find that the newer memory model scales poorly compared to the earlier, less accurate model. Next, we investigate ho...

• Type: Conference
• Year: 2009
• Where: VMCAI
• Authors: Zvonimir Rakamaric, Alan J. Hu
• Keywords: Memory Accesses, Memory Model, Scalable Memory Model, Software Engineering, VMCAI 2009