Encoding floating-points using the SMT theory in ESBMC: An empirical evaluation over the SV-COMP benchmarks
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 (Math...
| मुख्य लेखकों: | , , |
|---|---|
| स्वरूप: | Conference item |
| प्रकाशित: |
Springer, Cham
2017
|