登陆
注册
工具列表
Tool list
CBMC
2020-06-01
293
-
基于有界模型检测的C/C++程序内存泄露检测
C/C++语言中的动态内存管理机制自由且灵活,但动态内存的使用容易引入内存泄露,导致系统性能降低甚至系统崩溃。为了更加有效地检测内存泄露,提出了一个基于有界模型检测技术的C/C++程序内存泄露检测方案...
-
Test Data Generation for Cyclic Executives with CBMC and Frama-C: A Case Study
Testers of cyclic executive systems are required to make considerable and repetitive efforts to dete...
-
模型检验在航天测控软件上的应用研究
模型检验是确保程序质量的有效手段,能弥补软件测试的不足。但航天测控软件规模大、输入数据复杂、验证性质不明确等因素极大地阻碍了模型检验的应用。针对航天测控软件,分析了其特点以及对其执行模型检验的困难,提...
