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

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.

Bibliographical metadata

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

Publication series

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