近期堆内存规约与验证技术综述
计算机科学中的逻辑
2022-03-25 v2 符号计算
摘要
本文概述了现有的动态内存验证方法;进行了对比分析;评估了其在解决动态内存控制、监测与验证问题上的适用性。本文分为八个部分。第一部分介绍形式化验证,随后一节讨论动态内存管理问题。第三部分讨论由堆变换扩展到栈的Hoare演算。第五和第六部分介绍动态内存形状分析与指针旋转的概念。第七部分关于分离逻辑。最后一部分讨论了进一步研究的可能领域,特别是对象各类实例在记录层的识别;证明的自动化;“热”代码,即程序运行时自我更新的软件代码;增强直观性,例如证明解释方面。
引用
@article{arxiv.1910.10176,
title = {Review of Recent Heap Specification and Verification Techniques},
author = {René Haberland},
journal= {arXiv preprint arXiv:1910.10176},
year = {2022}
}
备注
fully translated preprint (English); final journal paper 26 pages (in Russian)