In a broad sense, formal methods are mathematically rigorous techniques used to describe, monitor, and check system properties and limitations in computer systems, along with the fields in which these techniques can generally be applied, guidelines for how these techniques can be used, and tools or software used in the implementation of these techniques. One application of formal methods is in monitoring and checking the propagation of errors in computational programs. Due to the limits of finite precision arithmetic, as one works with floating-point representations of real numbers in computer programs, round-off errors tend to accumulate under mathematical operations and may become unacceptably large. Symbolic Taylor Error Expressions is a technique used in the tool FPTaylor to soundly bound the round-off error of mathematical operators which provide a good trade-off between efficiency and accuracy.
In this presentation, I will give a general overview to formal methods, the history of formal methods, and how formal methods are applied in various fields of engineering and industry. Afterwards, I will present a formally verified implementation of Symbolic Taylor Error Expressions in a specification language, automated theorem prover, and typechecker called Prototype Verification System (PVS). I will also go over how these error expressions can be used in PRECiSA, a prototype static analysis tool that can compute verified round-off error bounds for floating-point programs. Time permitting, I will introduce other theorems, properties, and structures which I have proven in PVS for inclusion in the NASA PVS Library.