- Tytuł:
- Foundational Certification of Code Transformations Using Automatic Differentiation
- Autorzy:
-
Tadjouddine, E. M.
Lv, W. - Powiązania:
- https://bibliotekanauki.pl/articles/305770.pdf
- Data publikacji:
- 2014
- Wydawca:
- Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
- Tematy:
-
relational Hoare logic
abductive reasoning
certification
automatic differentiation - Opis:
- 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 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.
- Źródło:
-
Computer Science; 2014, 15 (2); 215-236
1508-2806
2300-7036 - Pojawia się w:
- Computer Science
- Dostawca treści:
- Biblioteka Nauki
Artykuł