TY - CONF
T1 - ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory
T2 - (Competition Contribution)
AU - Menezes, Rafael
AU - Cordeiro, Lucas
AU - Gadelha, Mikhail R
AU - Monteiro, Felipe R.
AU - Nicole, Denis
PY - 2020
Y1 - 2020
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.
U2 - 10.1007/978-3-030-45234-6_27
DO - 10.1007/978-3-030-45234-6_27
M3 - Paper
SP - 525
EP - 529
ER -