Conference item icon

Conference item

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

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

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Accepted Manuscript

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-319-70848-5_7

Authors


Gadelha, MYR More by this author
More by this author
Department:
Oxford, MPLS, Computer Science
Nicole, DA More by this author
Publisher:
Springer, Cham Publisher's website
Volume:
10623
Pages:
91-106
Series:
Lecture Notes in Computer Science
Publication date:
2017-11-11
Acceptance date:
2017-09-08
DOI:
ISSN:
0302-9743
Pubs id:
pubs:726194
URN:
uri:c1e91379-1990-491d-94fa-e497e7a8a26d
UUID:
uuid:c1e91379-1990-491d-94fa-e497e7a8a26d
Local pid:
pubs:726194
ISBN:
978-3-319-70848-5

Terms of use


Metrics



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

TO TOP