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.
CITATION STYLE
Gadelha, M. R., Menezes, R., Monteiro, F. R., Cordeiro, L. C., & Nicole, D. (2020). Esbmc: Scalable and precise test generation based on the floating-point theory: (competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12076 LNCS, pp. 525–529). Springer. https://doi.org/10.1007/978-3-030-45234-6_27
Mendeley helps you to discover research relevant for your work.