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

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

C/C Program Memory Leak Detection Based on Bounded Model Checking

The dynamic memory management mechanism in C/C programming language is free and flexible, but when used by developer it is easy to introduce memory leaks which lead to performance degradation and even failure of system. In order to detect memory leak more effectively, a memory leak detection method based on bounded model checking for C program called MLD-CBMC was proposed. It took C/C program files as input, unwound the program and inserted memory leak properties, encoded the program constraints and properties into verification conditions using satisfiability modulo theory, then passed the verification conditions to a SMT solver. Thus it converted detecting memory leaks to solving satisfiability problems. By experiment and cooperation with other bounded model checking tools, MLD-CBMC shows its feasibility and effectiveness.