ESBMC v7.4：利用区间的力量
软件工程
2023-12-25 v1
摘要
ESBMC实现了许多最先进的模型检测技术。我们报告了新的和改进的特性，这些特性使我们能够获得以前不支持的程序和属性的验证结果。ESBMC采用了一种新的程序表达式静态区间分析，以提高验证性能。这包括基于区间的布尔和整数推理、前向和后向收缩器，以及由于单例区间的普遍性而进行的特定优化。其他相关改进涉及并发程序的验证，以及若干操作模型、内部模型以及库（如pthread和C数学库）的模型。扩展的内存安全分析现在允许跟踪仍被视为可达的内存泄漏。
引用
@article{arxiv.2312.14746,
title = {ESBMC v7.4: Harnessing the Power of Intervals},
author = {Rafael Menezes and Mohannad Aldughaim and Bruno Farias and Xianzhiyu Li and Edoardo Manino and Fedor Shmarov and Kunjian Song and Franz Brauße and Mikhail R. Gadelha and Norbert Tihanyi and Konstantin Korovin and Lucas C. Cordeiro},
journal= {arXiv preprint arXiv:2312.14746},
year = {2023}
}