C语言作为一种广泛使用的低级语言，支持直接的内存操作，因此内存模型对于其语义的形式化和程序验证至关重要。在软件工程中，确保程序的可信度，即其按预期行为运行，对软件开发而言是一个基础且必要的步骤。形式化方法验证程序，是通过数学的手段确保软件可信的重要手段，而这一切需要一个合适的内存模型作为基础。
传统的字节内存模型能够很好地描述各种内存操作，但存在无法保证安全性和使得程序验证变得复杂的问题。它没有提供足够的抽象级别，难以捕捉低级语言中的高级概念，如类型安全、内存别名分析和指针操作等。
面向对象语言的内存模型通常具有较高的抽象级别，这使得程序验证变得更为简单，但这样的内存模型并不适合描述低级的内存操作。面向对象语言往往屏蔽了内存操作的细节，但这对于性能敏感且需要直接内存操作的语言来说是不足的。
鉴于此，何炎祥等人提出了一种结合了字节级内存模型和面向对象内存模型的新型安全类型化内存模型。这种模型旨在结合两者的优势：能够描述低级内存操作（如指针算术、结构赋值、类型转换等），同时又提供足够的抽象级别，以利于程序验证。
在形式化验证领域，霍尔逻辑（Hoare Logic）是一种常用的逻辑系统，它通过一组形式化规则来描述程序如何根据其操作的前件和后件来改变状态。霍尔逻辑通常用于证明程序的特定属性，尤其是在内存操作的正确性和安全性方面。而安全的类型化内存模型允许基于霍尔逻辑的程序验证，降低了验证过程的复杂度，并使程序更易于分析和验证。
文章指出，新的内存模型不仅可以用于程序验证，而且在形式化语义方面也有贡献。这是通过允许指针算术、结构赋值、类型转换等操作来完成的，这些操作在传统的内存模型中可能引起复杂性问题。通过这种方式，新的内存模型减少了指针别名问题带来的验证难度，提高了内存操作的可预测性。
为了形式化实现和验证提出的内存模型，研究人员使用了Coq证明助手。Coq是一个强大的、被广泛认可的形式化证明工具，用于进行逻辑推理和数学证明。使用Coq对内存模型进行形式化和验证，可以确保模型的正确性，并为基于此模型的程序验证提供坚实的基础。
程序语言的语义是对程序运行时行为的精确描述。为确保软件的预期运行，必须对程序语言的语义进行形式化，这样程序才能无歧义地按照定义好的规则执行。语义的形式化是保证软件可信的关键步骤，尤其是在涉及低级内存操作的语言中更是如此。
中图法分类号TP311属于计算机软件及计算机应用这一大类，涵盖了与软件开发、维护和应用相关的各类研究。在这一分类下，涉及到程序语言的语义研究，有助于更好地理解语言的运行时行为，从而设计出更安全、更高效的程序。
文章中提及的国家自然科学基金项目为研究工作提供了支持，反映了该研究在学术界所得到的认可和重视。通信作者吴伟的邮箱地址提供了一种方式，以便于学术交流和讨论。通过邮件联系，研究人员和读者可以针对该内存模型的进一步问题或合作进行沟通。
提出的安全类型化内存模型是对传统内存模型的创新性改进，它既能够描述复杂的低级内存操作，又具备了足够的抽象性，以利于形式化验证。这种模型的提出和验证，为C语言及其类似环境下的程序验证提供了新的工具和理论基础，极大地促进了该领域的发展。
