VerifiedValidatedNumericalMethods

Verified Validated Numerical Methods

MSc thesis project idea, Cezar Ionescu, 2015-03-17

In current terminology, "validated numerical methods" are those which can be proven to be correct when taking into account the limited-precision operations available on computers; the most important example is that of interval-based methods. "Verified software", on the other hand, is software for which we have a machine-checked proof of correctness. Theses in this area will investigate the possibility of having both "validation" and "verification", by, e.g., implementing basic interval-based methods in Agda.