@article{ME66B4C4D,
title = "Memory Model Design for Integer-Pointer Casting Support in C-like languages Via Dual Non-determinism",
journal = "Journal of KIISE, JOK",
year = "2024",
issn = "2383-630X",
doi = "10.5626/JOK.2024.51.7.643",
author = "Yonghyun Kim, Chung-Kil Hur",
keywords = "software formal verification, formal model, compiler, memory model",
abstract = "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."
}