Foundational Certification of Code Transformations Using Automatic Differentiation

Emmanuel M. Tadjouddine, Wenjin Lv

Abstract


Automatic Differentiation (AD) is concerned with the semantics augmentation of an input program representing a function to form a transformed program that computes the function's derivatives.
To ensure the correctness  of the AD transformed code, particularly for safety critical applications, we aim at certifying the algebraic manipulations at the heart of the AD process. We have considered a WHILE-language and have shown how such proofs can be constructed by using an appropriate relational Hoare logic.
In particular, we have shown how such inference rules can be constructed for both the forward and reverse mode AD by using an abductive logical reasoning.

Full Text:

PDF


DOI: https://doi.org/10.7494/csci.2014.15.2.215

Refbacks

  • There are currently no refbacks.