Program Verification of Numerical Computation

TL;DR

This paper presents a formal verification method for numerical computation programs, laying the groundwork for the VPC software package to ensure correctness in numerically intensive applications.

Contribution

It introduces a formal framework and rules for verifying numerical programs, with initial results demonstrating basic machine arithmetic within this system.

Findings

Development of the VPC verification framework

Formal rules for numerical program correctness

Basic machine arithmetic results derived

Abstract

These notes outline a formal method for program verification of numerical computation. It forms the basis of the software package VPC in its initial phase of development. Much of the style of presentation is in the form of notes that outline the definitions and rules upon which VPC is based. The initial motivation of this project was to address some practical issues of computation, especially of numerically intensive programs that are commonplace in computer models. The project evolved into a wider area for program construction as proofs leading to a model of inference in a more general sense. Some basic results of machine arithmetic are derived as a demonstration of VPC.