Skip to Main content Skip to Navigation
Journal articles

Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study

Abstract : We report on a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving.
Document type :
Journal articles
Complete list of metadata

Cited literature [44 references]  Display  Hide  Download

https://hal.inria.fr/hal-00967124
Contributor : Claude Marché <>
Submitted on : Friday, March 28, 2014 - 9:08:45 AM
Last modification on : Thursday, July 8, 2021 - 3:47:43 AM
Long-term archiving on: : Saturday, June 28, 2014 - 10:56:34 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Claude Marché. Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study. Science of Computer Programming, Elsevier, 2014, 93 (3), pp.279-296. ⟨10.1016/j.scico.2014.04.003⟩. ⟨hal-00967124⟩

Share

Metrics

Record views

528

Files downloads

805