Verification of floating point programs

Duracz, Jan (2010). Verification of floating point programs. PHD thesis, Aston University.

Abstract

In this thesis we present an approach to automated verification of floating point programs. Existing techniques for automated generation of correctness theorems are extended to produce proof obligations for accuracy guarantees and absence of floating point exceptions. A prototype automated real number theorem prover is presented, demonstrating a novel application of function interval arithmetic in the context of subdivision-based numerical theorem proving. The prototype is tested on correctness theorems for two simple yet nontrivial programs, proving exception freedom and tight accuracy guarantees automatically. The prover demonstrates a novel application of function interval arithmetic in the context of subdivision-based numerical theorem proving. The experiments show how function intervals can be used to combat the information loss problems that limit the applicability of traditional interval arithmetic in the context of hard real number theorem proving.

Divisions: Engineering & Applied Sciences > Computer science
Additional Information: If you have discovered material in AURA which is unlawful e.g. breaches copyright, (either yours or that of a third party) or any other law, including but not limited to those relating to patent, trademark, confidentiality, data protection, obscenity, defamation, libel, then please read our Takedown Policy and contact the service immediately.
Institution: Aston University
Uncontrolled Keywords: static analysis,floating point,formal software verification,automated theorem proving
Completed Date: 2010
Authors: Duracz, Jan

Download

[img]

[img]

Access Restriction: Restricted to Repository staff only


Export / Share Citation


Statistics

Additional statistics for this record