A Scalable Memory Model for Low-Level Code
Source: University of British Columbia
Because of critical importance underlying all other software, low level 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 investigations to develop an accurate (i.e., providing a useful level of soundness and precision).