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

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, th...

Descripción completa

Detalles Bibliográficos
Autores principales: Gadelha, Mikhail R., Menezes, Rafael, Monteiro, Felipe R., Cordeiro, Lucas C., Nicole, Denis
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7418142/
http://dx.doi.org/10.1007/978-3-030-45234-6_27
_version_ 1783569634742501376
author Gadelha, Mikhail R.
Menezes, Rafael
Monteiro, Felipe R.
Cordeiro, Lucas C.
Nicole, Denis
author_facet Gadelha, Mikhail R.
Menezes, Rafael
Monteiro, Felipe R.
Cordeiro, Lucas C.
Nicole, Denis
author_sort Gadelha, Mikhail R.
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7418142
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74181422020-08-11 ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory: (Competition Contribution) Gadelha, Mikhail R. Menezes, Rafael Monteiro, Felipe R. Cordeiro, Lucas C. Nicole, Denis Fundamental Approaches to Software Engineering Article 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. 2020-03-13 /pmc/articles/PMC7418142/ http://dx.doi.org/10.1007/978-3-030-45234-6_27 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Gadelha, Mikhail R.
Menezes, Rafael
Monteiro, Felipe R.
Cordeiro, Lucas C.
Nicole, Denis
ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory: (Competition Contribution)
title ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory: (Competition Contribution)
title_full ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory: (Competition Contribution)
title_fullStr ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory: (Competition Contribution)
title_full_unstemmed ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory: (Competition Contribution)
title_short ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory: (Competition Contribution)
title_sort esbmc: scalable and precise test generation based on the floating-point theory: (competition contribution)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7418142/
http://dx.doi.org/10.1007/978-3-030-45234-6_27
work_keys_str_mv AT gadelhamikhailr esbmcscalableandprecisetestgenerationbasedonthefloatingpointtheorycompetitioncontribution
AT menezesrafael esbmcscalableandprecisetestgenerationbasedonthefloatingpointtheorycompetitioncontribution
AT monteirofeliper esbmcscalableandprecisetestgenerationbasedonthefloatingpointtheorycompetitioncontribution
AT cordeirolucasc esbmcscalableandprecisetestgenerationbasedonthefloatingpointtheorycompetitioncontribution
AT nicoledenis esbmcscalableandprecisetestgenerationbasedonthefloatingpointtheorycompetitioncontribution

Ejemplares similares