Verifying the Floating-Point Computation Equivalence of Manually and Automatically Differentiated Code

The semantics of floating-point computations are known to be difficult to verify. Software verification tools often provide little or no support for floating-point semantics, making it difficult to prove the correctness of an optimized variant of a program involving floating-point computations. In this paper we present an approach for verifying the equivalence of two program variants involving non-trivial floating-point operations. The selected test case for our approach are two variants of a differentiated code - one automatically generated, the other manually written. The verification technique operates at the source level, therefore we also investigate the generated assembly code variants and reason on a set of selected compiler options and architectures to guarantee that the correctness proof also holds for the generated binaries.