An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

Mikhail R Gadelha; Lucas Cordeiro; Denis A Nicole

An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

Mikhail R Gadelha
, Lucas Cordeiro
, Denis A Nicole

Formal Methods

SIDIA Instituto de Ciência e Tecnologia
University of Southampton

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

We describe a new SMT bit-blasting API for floating-point programs and evaluate it using different off-the-shelf SMT solvers during the verification of several C programs. The new floating-point API is part of the SMT backend in ESBMC, a state-of-the-art bounded model checker for C and C++. For the evaluation, we compared our floatingpoint API against the native floating-point APIs in Z3 and MathSAT. We show that Boolector, when using our new
oating-point API, outperforms the solvers with native support for
oating-points, correctly verifying more programs in less time. Experimental results also show that our floating-point API implemented in ESBMC is on par with other state-of-the-art software verifiers. Furthermore, when verifying programs with floating-point arithmetic, our new floating-point API produced no
wrong answers.

Original language	English
Title of host publication	13th Workshop on Numerical Software Verification
Publication status	Accepted/In press - 23 Jun 2020
Event	13th Workshop on Numerical Software Verification - Duration: 20 Jul 2020 → 21 Jul 2020

Workshop

Workshop	13th Workshop on Numerical Software Verification
Period	20/07/20 → 21/07/20

Keywords

floating-point arithmetic
satisfiability modulo theories
software verification

Embargoed Document

nsv2020
Accepted author manuscript, 356 KB
Embargo ends: 1/01/30

Cite this

@inproceedings{ae6496ad22f741f2a729b8214970a50e,

title = "An Efficient Floating-Point Bit-Blasting API for Verifying C Programs",

abstract = "We describe a new SMT bit-blasting API for floating-point programs and evaluate it using different off-the-shelf SMT solvers during the verification of several C programs. The new floating-point API is part of the SMT backend in ESBMC, a state-of-the-art bounded model checker for C and C++. For the evaluation, we compared our floatingpoint API against the native floating-point APIs in Z3 and MathSAT. We show that Boolector, when using our new oating-point API, outperforms the solvers with native support for oating-points, correctly verifying more programs in less time. Experimental results also show that our floating-point API implemented in ESBMC is on par with other state-of-the-art software verifiers. Furthermore, when verifying programs with floating-point arithmetic, our new floating-point API produced no wrong answers.",

keywords = "floating-point arithmetic, satisfiability modulo theories, software verification",

author = "Gadelha, \{Mikhail R\} and Lucas Cordeiro and Nicole, \{Denis A\}",

year = "2020",

month = jun,

day = "23",

language = "English",

booktitle = "13th Workshop on Numerical Software Verification",

note = "13th Workshop on Numerical Software Verification ; Conference date: 20-07-2020 Through 21-07-2020",

}

TY - GEN

T1 - An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

AU - Gadelha, Mikhail R

AU - Cordeiro, Lucas

AU - Nicole, Denis A

PY - 2020/6/23

Y1 - 2020/6/23

N2 - We describe a new SMT bit-blasting API for floating-point programs and evaluate it using different off-the-shelf SMT solvers during the verification of several C programs. The new floating-point API is part of the SMT backend in ESBMC, a state-of-the-art bounded model checker for C and C++. For the evaluation, we compared our floatingpoint API against the native floating-point APIs in Z3 and MathSAT. We show that Boolector, when using our new oating-point API, outperforms the solvers with native support for oating-points, correctly verifying more programs in less time. Experimental results also show that our floating-point API implemented in ESBMC is on par with other state-of-the-art software verifiers. Furthermore, when verifying programs with floating-point arithmetic, our new floating-point API produced no wrong answers.

AB - We describe a new SMT bit-blasting API for floating-point programs and evaluate it using different off-the-shelf SMT solvers during the verification of several C programs. The new floating-point API is part of the SMT backend in ESBMC, a state-of-the-art bounded model checker for C and C++. For the evaluation, we compared our floatingpoint API against the native floating-point APIs in Z3 and MathSAT. We show that Boolector, when using our new oating-point API, outperforms the solvers with native support for oating-points, correctly verifying more programs in less time. Experimental results also show that our floating-point API implemented in ESBMC is on par with other state-of-the-art software verifiers. Furthermore, when verifying programs with floating-point arithmetic, our new floating-point API produced no wrong answers.

KW - floating-point arithmetic

KW - satisfiability modulo theories

KW - software verification

M3 - Conference contribution

BT - 13th Workshop on Numerical Software Verification

T2 - 13th Workshop on Numerical Software Verification

Y2 - 20 July 2020 through 21 July 2020

ER -

An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

Abstract

Workshop

Keywords

Embargoed Document

Fingerprint

Cite this