Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Computer Science

1 2014

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: relational Hoare logic

Sortuj według:

Ogranicz wyniki do:

Foundational Certification of Code Transformations Using Automatic Differentiation

Tadjouddine E. M., Lv W.

Computer Science

2014

Vol. 15 (2)

215--236

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.