ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backward contractors, and particular optimizations related to singleton intervals because of their ubiquity. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.

翻译：ESBMC 实现了许多用于模型检验的最新技术。我们报告了新的和改进的功能，这些功能使我们能够获得之前不支持的程序和属性的验证结果。ESBMC 采用了一种新的程序表达式静态区间分析以提高验证性能。这包括基于布尔值和整数的区间推理、前向和后向紧缩算子，以及由于单例区间的普遍性而进行的特定优化。其他相关改进涉及并发程序的验证，以及若干操作模型、内部模型，以及诸如pthread和C数学库等库的模型。扩展的内存安全性分析现在能够跟踪仍被视为可达的内存泄漏。