Encoding floating-points using the SMT theory in ESBMC: An empirical evaluation over the SV-COMP benchmarks

Conference item

Abstract:: This paper describes the support for encoding C/C++ programs using the SMT theory of floating-point numbers in ESBMC: an SMT-based context-bounded model checker that provides bit-precise verification of C and C++ programs. In particular, we exploit the availability of two different SMT solvers (MathSAT and Z3) to discharge and check the verification conditions produced by our encoding using the benchmarks from the International Competition on Software Verification (SV-COMP). The experimental results show that our encoding based on MathSAT is able to outperform not only Z3, but also other existing approaches that participated in the most recent edition of SV-COMP.

Files:: sbmf2017_02.pdf

(Preview, Accepted manuscript, pdf, 740.3KB, Terms of use)

Publisher:: Springer, Cham
Host title:: SBMF 2017: Formal Methods: Foundations and Applications
Journal:: SBMF 2017 : 20th Brazilian Symposium on Formal Methods More from this journal
Volume:: 10623
Pages:: 91-106
Series:: Lecture Notes in Computer Science
Publication date:: 2017-11-11
Acceptance date:: 2017-09-08
DOI:: 10.1007/978-3-319-70848-5_7
ISSN:: 0302-9743
ISBN:: 9783319708485

Keywords:: satisfiability modulo theories

formal methods

floating-point arithmetic

software verification
Pubs id:: pubs:726194
UUID:: uuid:c1e91379-1990-491d-94fa-e497e7a8a26d
Local pid:: pubs:726194
Source identifiers:: 726194
Deposit date:: 2017-09-11

Copyright holder:: Springer International Publishing AG
Notes:: Copyright © 2017 Springer International Publishing AG. This is the accepted manuscript version of the paper. The final version is available online from Springer at: https://doi.org/10.1007/978-3-319-70848-5_7

Licence:: Terms and Conditions of Use for Oxford University Research Archive

If you are the owner of this record, you can report an update to it here: Report update to this record