# ESBMC v7.4: Harnessing the Power of Intervals

arXiv: https://arxiv.org/abs/2312.14746 · HTML: https://mlsanity.com/paper/2312.14746/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Dec 2023.

## Built on by (most cited first, 6 of 6)

- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview](https://mlsanity.com/paper/2503.10784/) (2025)
- [Floating-Point Neural Network Verification at the Software Level](https://mlsanity.com/paper/2510.23389/) (2025)
- [ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification](https://mlsanity.com/paper/2605.27051/) (2026)
- [MFH: A Multi-faceted Heuristic Algorithm Selection Approach for Software Verification](https://mlsanity.com/paper/2503.22228/) (2025)

## Abstract (arXiv)

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.