White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Static analysis for detecting and avoiding floating-point run-time errors in logic programs

Nunez Fontarnau, Javier (2006) Static analysis for detecting and avoiding floating-point run-time errors in logic programs. PhD thesis, University of Leeds.


Download (1242Kb)


The aim of this thesis is to provide techniques for the abstraction of floating-point expressions into the polyhedra domain as well as into the finite powerset of polyhedra domain. Moreover, this thesis aims at presenting a forward and a backward analysis for the detection and inference of floating-point errors such as overflow and division by zero. These techniques are based on abstract interpretation, which is a theory for the sound approximation of the semantics of programs. These abstractions and analyses have important applications for instance in engineering, mechanics and computer aided graphics design. The abstraction of floating-point expressions into polyhedra includes two stages. the first, we present an approximation of floating-point expression by a polynomial with interval coefficients that includes the possible floating-point errors. In the second stage we present techniques for abstracting polynomials with interval coefficients into polyhedra and polyhedra powersets. Moreover, we present a technique for abstracting expressions in which a division by zero may occur. A forward analysis for the detection of overflow and division by zero is then presented. This analysis is particular in that it always reaches the output of a programs. This an important requirement since the backward analysis needs information on the output to infer which input to a program could cause an overflow or a division by zero. Such analyses are important especially in the design of systems with high contents of nonlinear floating-point expressions. Experimental results show the usability of these analyses.

Item Type: Thesis (PhD)
Additional Information: Supplied directly by the School of Computing, University of Leeds.
Academic Units: The University of Leeds > Faculty of Engineering (Leeds) > School of Computing (Leeds)
Identification Number/EthosID: uk.bl.ethos.435813
Depositing User: Dr L G Proll
Date Deposited: 24 Mar 2011 15:30
Last Modified: 07 Mar 2014 11:23
URI: http://etheses.whiterose.ac.uk/id/eprint/1347

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)