Termination analysis of floating-point programs using parameterizable rational approximations

Fonenantsoa Maurica; Frédéric Mesnard; Etienne Payet

Termination analysis of floating-point programs using parameterizable rational approximations

Fonenantsoa Maurica ¹ Frédéric Mesnard ¹ Etienne Payet ¹

1 LIM - Laboratoire d'Informatique et de Mathématiques

Abstract : Analysis of floating-point programs is a topic that received an increasing attention the past few years. However, only very few works have been done regarding their termination analysis. We address that problem in this paper. We present a technique that takes advantage of the already existing works on termination analysis of rational programs. Our approach consists in translating the floating-point programs into rational ones by means of sound approximations. We approximate the floating-point expressions using piecewise linear functions. Our approximation differs from the already existing ones in the sense that it can be as precise as needed.

Keywords : Software verification Keywords Termination analysis Floating-point arithmetic Lineariza-tion

Document type :

Conference papers

Domain :

Computer Science [cs]

Complete list of metadatas

Cited literature [16 references] Display Hide Download

http://hal.univ-reunion.fr/hal-01451687
Contributor : Réunion Univ <>
Submitted on : Monday, November 5, 2018 - 11:00:36 AM
Last modification on : Thursday, March 28, 2019 - 11:24:10 AM
Long-term archiving on : Wednesday, February 6, 2019 - 2:37:04 PM

sac16.pdf

Files produced by the author(s)

Termination analysis of floating-point programs using parameterizable rational approximations

File

Identifiers

Collections

Citation

Export

Metrics

43

55

Contact

Termination analysis of floating-point programs using parameterizable rational approximations

File

Identifiers

Collections

Citation

Export

Share

Metrics

43

55

Contact