ESBMC: Scalable and Precise Test-Case Generation based on the Floating-Point Theory

Mikhail R  Gadelha; Rafael Menezes; Felipe R.  Monteiro; Lucas Cordeiro; Denis  Nicole

ESBMC: Scalable and Precise Test-Case Generation based on the Floating-Point Theory

Mikhail R Gadelha, Rafael Menezes, Felipe R. Monteiro, Lucas Cordeiro, Denis Nicole

Formal Methods

SIDIA Instituto de Ciência e Tecnologia

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

Abstract

ESBMC is an SMT-based bounded model checker for real-world C programs. Such programs often represent real numbers using the floating-points, most commonly, the IEEE floating-point standard (IEEE 754-2008). Thus, ESBMC now includes a new floating-point arithmetic encoding layer in our SMT backend, that encodes floating-point operations into bit-vector operations. In particular, ESBMC can use off-the-shelf SMT solvers that offer support for bit-vectors only to encode floating-point arithmetic.

Original language	English
Title of host publication	23rd International Conference on Fundamental Approaches to Software Engineering (FASE)
Publication status	Accepted/In press - 21 Feb 2020

Embargoed Document

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

Cite this

@inproceedings{92fe0175007e4d9487e42e34b0e6e103,

title = "ESBMC: Scalable and Precise Test-Case Generation based on the Floating-Point Theory",

abstract = "ESBMC is an SMT-based bounded model checker for real-world C programs. Such programs often represent real numbers using the floating-points, most commonly, the IEEE floating-point standard (IEEE 754-2008). Thus, ESBMC now includes a new floating-point arithmetic encoding layer in our SMT backend, that encodes floating-point operations into bit-vector operations. In particular, ESBMC can use off-the-shelf SMT solvers that offer support for bit-vectors only to encode floating-point arithmetic.",

author = "Gadelha, \{Mikhail R\} and Rafael Menezes and Monteiro, \{Felipe R.\} and Lucas Cordeiro and Denis Nicole",

year = "2020",

month = feb,

day = "21",

language = "English",

booktitle = "23rd International Conference on Fundamental Approaches to Software Engineering (FASE)",

}

TY - GEN

T1 - ESBMC: Scalable and Precise Test-Case Generation based on the Floating-Point Theory

AU - Gadelha, Mikhail R

AU - Menezes, Rafael

AU - Monteiro, Felipe R.

AU - Cordeiro, Lucas

AU - Nicole, Denis

PY - 2020/2/21

Y1 - 2020/2/21

N2 - ESBMC is an SMT-based bounded model checker for real-world C programs. Such programs often represent real numbers using the floating-points, most commonly, the IEEE floating-point standard (IEEE 754-2008). Thus, ESBMC now includes a new floating-point arithmetic encoding layer in our SMT backend, that encodes floating-point operations into bit-vector operations. In particular, ESBMC can use off-the-shelf SMT solvers that offer support for bit-vectors only to encode floating-point arithmetic.

AB - ESBMC is an SMT-based bounded model checker for real-world C programs. Such programs often represent real numbers using the floating-points, most commonly, the IEEE floating-point standard (IEEE 754-2008). Thus, ESBMC now includes a new floating-point arithmetic encoding layer in our SMT backend, that encodes floating-point operations into bit-vector operations. In particular, ESBMC can use off-the-shelf SMT solvers that offer support for bit-vectors only to encode floating-point arithmetic.

M3 - Conference contribution

BT - 23rd International Conference on Fundamental Approaches to Software Engineering (FASE)

ER -

ESBMC: Scalable and Precise Test-Case Generation based on the Floating-Point Theory

Abstract

Embargoed Document

Fingerprint

Cite this