Block-Abstraction Memoization for Symbolic Memory Graphs

Block-Abstraction Memoization for Symbolic Memory Graphs

Petrov O.M. (ISP RAS, Moscow, Russia)

Abstract

This paper considers program analysis based on symbolic memory graphs (SMG) and Block-Abstraction Memoization (BAM) technique which enables procedure summarization. Both SMG and BAM are implemented in static software verification framework CPAchecker. SMG analysis models program memory as a graph with edges between objects in memory and symbolic values. Using it, violations of memory safety can be found in real-world programs such as Linux drivers. With BAM, any given analysis can make a summary of a block (a function or a loop) and reuse the block summary when it enters a block with similar enough context. This paper enables SMG to work with BAM. Several ways to distinguish context are introduced and compared against each other and baseline SMG analysis without BAM. We hope to improve efficiency of the analysis using BAM in future work.

Keywords

formal software verification; software model checking; CPAchecker; symbolic memory graphs; block abstraction; procedure summarization.

Edition

Proceedings of the Institute for System Programming, vol. 38, issue 5, 2026, pp. 337-350

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(5)-19

For citation

Petrov O.M. Block-Abstraction Memoization for Symbolic Memory Graphs. Proceedings of the Institute for System Programming, vol. 38, issue 5, 2026, pp. 337-350 DOI: 10.15514/ISPRAS-2026-38(5)-19.

Full text of the paper in pdf Back to the contents of the volume