Yonghyun Kim  Chung-Kil Hur

10.5626/JOK.2024.51.7.643

software formal verification Formal Model Compiler memory model

In system programming, pointers are essential elements. However, applying formal verification methods to programs involving integer-pointer casting poses an important challenge. To address this challenge, a mathematically defined memory model that supports integer-pointer casting, along with proof techniques for verification, is necessary. This study presents a memory model that supports integer-pointer casting within the Coq proof assistant. The model accommodates patterns associated with integer-pointer operations, including one-past-the-end pointers. Additionally, a simulation-based proof technique is introduced, which enables the utilization of the model for program verification. The adequacy of this technique is established through proof. To validate the effectiveness of the approach, the defined memory model is integrated into CompCert, a verified C compiler, replacing its original memory model. Subsequently, two proofs of CompCert's optimization verification are updated using the simulation technique. It is anticipated that the proposed memory model will find applications in program and compiler verification tasks involving integer-pointer operations.