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

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: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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 language	English
Title of host publication	30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Publication status	Accepted/In press - 10 Feb 2024

Embargoed Document

tacas2024 (1)
Accepted author manuscript, 202 KB
Licence: CC BY
Embargo ends: 30/04/25

Cite this

@inproceedings{11cceb2702684f72baabc4dcefd02bbe,

title = "ESBMC v7.4: Harnessing the Power of Intervals (Competition Contribution)",

abstract = "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.",

author = "Rafael Menezes and Mohannad Aldughaim and Bruno Farias and Xianzhiyu Li and Edoardo Manino and Fedor Shmarov and Kunjian Song and Franz Brau{\ss}e and Gadelha, {Mikhail R.} and Norbert Tihanyi and Konstantin Korovin and Lucas Cordeiro",

year = "2024",

month = feb,

day = "10",

language = "English",

booktitle = "30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems",

}

TY - GEN

T1 - ESBMC v7.4

T2 - Harnessing the Power of Intervals (Competition Contribution)

AU - Menezes, Rafael

AU - Aldughaim, Mohannad

AU - Farias, Bruno

AU - Li, Xianzhiyu

AU - Manino, Edoardo

AU - Shmarov, Fedor

AU - Song, Kunjian

AU - Brauße, Franz

AU - Gadelha, Mikhail R.

AU - Tihanyi, Norbert

AU - Korovin, Konstantin

AU - Cordeiro, Lucas

PY - 2024/2/10

Y1 - 2024/2/10

N2 - 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.

AB - 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.

M3 - Conference contribution

BT - 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

ER -

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

Abstract

Embargoed Document

Fingerprint

Cite this