Verifying the Floating-Point Computation Equivalence of
Manually and Automatically Differentiated Code
Author/Presenters
Event Type
Workshop
Applications
Correctness
Debugging
Reliability
SIGHPC Workshop
Verification
TimeSunday, November 12th11:55am -
12:12pm
Location501
DescriptionThe 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.
