ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory
Mikhail R. Gadelha, Rafael Menezes, Felipe R. Monteiro, Lucas Carvalho Cordeiro, Denis A. Nicole · Lecture notes in computer science · 2020
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.