Construction of a Memory Safety Model for Concurrent Programs Based on Formal Verification

Abstract

As multi-core processors become the mainstream in computing, the memory safety issues of concurrent programs have grown increasingly severe due to their nondeterministic interactions. Formal verification, which provides rigorous guarantees for program correctness through mathematical methods, serves as a key approach to addressing this challenge. This paper aims to systematically construct a memory safety model for concurrent programs based on formal verification. The research first clarifies the formal definitions of spatial and temporal safety in concurrent environments and precisely characterizes shared memory interactions based on interleaving semantics and operational semantics. Subsequently, a modeling approach oriented toward concurrent memory safety is proposed, including abstract state machine modeling, logical representation of execution traces, and an extended separation logic resource specification framework. Finally, the study investigates automatic construction and refinement strategies for model invariants, explores verification algorithms such as symbolic execution and abstract interpretation, and designs a modular, extensible verification framework. This research provides a comprehensive technical pathway from theory to methodology for the systematic verification of concurrent memory safety.