ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory: (Competition Contribution)

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

Research output: Contribution to conferencePaperpeer-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 languageEnglish
Pages525-529
Number of pages5
DOIs
Publication statusPublished - 2020

Fingerprint

Dive into the research topics of 'ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory: (Competition Contribution)'. Together they form a unique fingerprint.

Cite this