Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Bibliographical metadata

Original languageEnglish
Title of host publicationBrazilian Symposium on Formal Methods
Publication statusPublished - 2017

Publication series

NameFormal Methods: Foundations and Applications
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349