ESBMC v7.4: Harnessing the Power of Intervals (Competition Contribution)

Rafael Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Brauße, Mikhail R. Gadelha, Norbert Tihanyi, Konstantin Korovin, Lucas Cordeiro

Research output: Other contribution


ESBMC implements many state-of-the-art techniques that combine abstract interpretation and model checking. Here, we report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC now employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, and forward-backward contractors. 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.
Original languageEnglish
Publication statusPublished - 10 Feb 2024


Dive into the research topics of 'ESBMC v7.4: Harnessing the Power of Intervals (Competition Contribution)'. Together they form a unique fingerprint.

Cite this