Validation of a Formal Floating-Point Model for the Interactive Proof Assistant Isabelle/HOL

This thesis aims to validate the formal floating-point model implemented in the Higher-Order Logic (HOL) proof assistant Isabelle, according to the IEEE 754 Standard. By integrating a testing environment with the proof assistant, the generation and processing of a large quantity of test vectors is made possible, and the resulting empirical data can be collected and analyzed. As a result of previous research, a substantial amount of work has already been put into the construction of a testing framework tailored specifically for Isabelle’s formal floating-point model. Therefore, the contribution of this thesis is mainly to utilize the framework for conducting the testing; however, certain additions and modifications to its components are also made. This includes adding support for testing comparison operations, as well as making the two floating-point formats half-precision (16-bit) and quadruple-precision (128-bit) available for testing. Furthermore, the framework is extended to allow for infinite deterministic testing of all combinations of formats, operations, and rounding modes that are implemented. A total of 116 combinations are tested simultaneously, and the results can be monitored in real time through a command line tool. The evaluation finds that all the properties of the formal model subject to testing can be considered validated. This conclusion is based on the empirical evidence pertaining to approximately 850 million processed test vectors, among which not a single one failed.