Verification of floating point programs

  • Jan Duracz

Student thesis: Doctoral ThesisDoctor of Philosophy

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.
Date of Award2010
Original languageEnglish
SupervisorMichal Konečný (Supervisor)

Keywords

  • static analysis
  • floating point
  • formal software verification
  • automated theorem proving

Cite this

Verification of floating point programs
Duracz, J. (Author). 2010

Student thesis: Doctoral ThesisDoctor of Philosophy