Foundational Certification Of Code Transformations Using Automatic Differentiation

Foundational Certification Of Code Transformations Using Automatic Differentiation

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, w...

Full description

Bibliographic Details
Main Authors: Emmanuel M. Tadjouddine, Wenjin Lv
Format: Article
Language:English
Published: AGH University of Science and Technology Press 2014-01-01
Series:Computer Science
Online Access:http://journals.agh.edu.pl/csci/article/download/756/881
id doaj-319667878fe8449d9d03b13b43c74634
record_format Article
spelling doaj-319667878fe8449d9d03b13b43c746342020-11-24T22:10:31ZengAGH University of Science and Technology PressComputer Science1508-28062014-01-0115221510.7494/csci.2014.15.2.215Foundational Certification Of Code Transformations Using Automatic DifferentiationEmmanuel M. Tadjouddine0Wenjin Lv1Xi’an Jiaotong-Liverpool University, Department of Computer Science & Software EngineeringXi’an Jiaotong-Liverpool University, Department of Computer Science & Software EngineeringAutomatic 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.http://journals.agh.edu.pl/csci/article/download/756/881
collection DOAJ
language English
format Article
sources DOAJ
author Emmanuel M. Tadjouddine
Wenjin Lv
spellingShingle Emmanuel M. Tadjouddine
Wenjin Lv
Foundational Certification Of Code Transformations Using Automatic Differentiation
Computer Science
author_facet Emmanuel M. Tadjouddine
Wenjin Lv
author_sort Emmanuel M. Tadjouddine
title Foundational Certification Of Code Transformations Using Automatic Differentiation
title_short Foundational Certification Of Code Transformations Using Automatic Differentiation
title_full Foundational Certification Of Code Transformations Using Automatic Differentiation
title_fullStr Foundational Certification Of Code Transformations Using Automatic Differentiation
title_full_unstemmed Foundational Certification Of Code Transformations Using Automatic Differentiation
title_sort foundational certification of code transformations using automatic differentiation
publisher AGH University of Science and Technology Press
series Computer Science
issn 1508-2806
publishDate 2014-01-01
description 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.
url http://journals.agh.edu.pl/csci/article/download/756/881
work_keys_str_mv AT emmanuelmtadjouddine foundationalcertificationofcodetransformationsusingautomaticdifferentiation
AT wenjinlv foundationalcertificationofcodetransformationsusingautomaticdifferentiation
_version_ 1725807764849033216

Similar Items