基于有界模型检测的C/C＋＋程序内存泄露检测

• 作者: 代声馨 徐保平 杨秋辉 洪玫 赵鹤 郭鑫宇 高婉玲 黄蔚
• 来源期刊: 计算机应用研究
• 关键词: C /C ++程序 内存泄露 有界模型检测 可满足性模理论
• 年，卷（期）: 2016,（6）
• 所属期刊栏目: 软件技术研究
• 页码范围: 1762-1766
• 页数: 5页
• 分类号: TP311.53
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2016.06.036

摘要

C ／C ＋＋语言中的动态内存管理机制自由且灵活，但动态内存的使用容易引入内存泄露，导致系统性能降低甚至系统崩溃。为了更加有效地检测内存泄露，提出了一个基于有界模型检测技术的 C ／C ＋＋程序内存泄露检测方案 MLD-CBMC。该方案以 C ／C ＋＋程序文件为输入，利用有界模型检测技术对程序进行展开处理，加入内存泄露性质，并利用可满足性模理论（SMT）对程序约束和性质组成的验证条件编码，使用 SMT 求解器对验证条件求解，将检测内存泄露问题转换为求解可满足性问题，实现 C ／C ＋＋程序内存泄露的检测。通过实验验证了方案的有效性，并与其他有界模型检测工具进行对比实验，实验证明方案对内存泄露的检测能力更强。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	洪玫	四川大学计算机学院	65	355	11.0	16.0
2	黄蔚	四川大学计算机学院	68	273	9.0	13.0
3	杨秋辉	四川大学计算机学院	20	159	7.0	12.0
4	代声馨	四川大学计算机学院	4	30	3.0	4.0
5	赵鹤	四川大学计算机学院	7	19	2.0	4.0
6	郭鑫宇	四川大学计算机学院	3	10	2.0	3.0
7	高婉玲	四川大学计算机学院	6	18	2.0	4.0
8	徐保平	四川大学计算机学院	2	21	2.0	2.0